From 50f97b0046e35554f33a9d44435c6171484292c4 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Mon, 14 Feb 2022 15:30:31 -0600 Subject: [PATCH] First shot at strict mode warnings --- prototyping/FFI/Data/Aeson.agda | 3 +- prototyping/Luau/AddrCtxt.agda | 4 +- prototyping/Luau/StrictMode.agda | 48 +++++++++++++++++ prototyping/Luau/Type.agda | 33 +++++++----- prototyping/Luau/Type/ToString.agda | 6 +-- prototyping/Luau/TypeCheck.agda | 29 +++++----- prototyping/Luau/VarCtxt.agda | 18 ++++--- prototyping/Properties.agda | 4 ++ prototyping/Properties/StrictMode.agda | 75 ++++++++++++++++++++++++++ prototyping/Properties/TypeCheck.agda | 17 +++--- 10 files changed, 194 insertions(+), 43 deletions(-) create mode 100644 prototyping/Luau/StrictMode.agda create mode 100644 prototyping/Properties/StrictMode.agda diff --git a/prototyping/FFI/Data/Aeson.agda b/prototyping/FFI/Data/Aeson.agda index 558c8a8c..0d90a8d5 100644 --- a/prototyping/FFI/Data/Aeson.agda +++ b/prototyping/FFI/Data/Aeson.agda @@ -6,7 +6,7 @@ open import Agda.Builtin.String using (String) open import FFI.Data.ByteString using (ByteString) open import FFI.Data.HaskellString using (HaskellString; pack) -open import FFI.Data.Maybe using (Maybe; just) +open import FFI.Data.Maybe using (Maybe; just; nothing) open import FFI.Data.Either using (Either; mapLeft) open import FFI.Data.Scientific using (Scientific) open import FFI.Data.Vector using (Vector) @@ -39,6 +39,7 @@ postulate {-# COMPILE GHC lookup = \_ -> Data.Aeson.KeyMap.lookup #-} postulate lookup-insert : ∀ {A} k v (m : KeyMap A) → (lookup k (insert k v m) ≡ just v) +postulate lookup-empty : ∀ {A} k → (lookup {A} k empty ≡ nothing) data Value : Set where object : KeyMap Value → Value diff --git a/prototyping/Luau/AddrCtxt.agda b/prototyping/Luau/AddrCtxt.agda index b3e9cb52..875ac5ca 100644 --- a/prototyping/Luau/AddrCtxt.agda +++ b/prototyping/Luau/AddrCtxt.agda @@ -4,7 +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) +open import Luau.VarCtxt using (orBot) AddrCtxt : Set AddrCtxt = Vector Type @@ -13,4 +13,4 @@ AddrCtxt = Vector Type ∅ = empty _[_] : AddrCtxt → Addr → Type -Σ [ a ] = orNone(lookup Σ a) +Σ [ a ] = orBot(lookup Σ a) diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda new file mode 100644 index 00000000..5b1ef4cf --- /dev/null +++ b/prototyping/Luau/StrictMode.agda @@ -0,0 +1,48 @@ +module Luau.StrictMode where + +open import Agda.Builtin.Equality using (_≡_) +open import Luau.Syntax using (Expr; Stat; Block; yes; nil; addr; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name) +open import Luau.Type using (Type; strict; bot; top; nil; _⇒_; tgt) +open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ) +open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) +open import Luau.TypeCheck(strict) using (_▷_⊢ᴮ_∋_∈_⊣_; _▷_⊢ᴱ_∋_∈_⊣_; var; addr; app; block; return; local) + +src : Type → Type +src = Luau.Type.src strict + +data Warningᴱ {Σ Γ S} : ∀ {M T Δ} → (Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → Set +data Warningᴮ {Σ Γ S} : ∀ {B T Δ} → (Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) → Set + +data Warningᴱ {Σ Γ S} where + + bot : ∀ {M T Δ} {D : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ} → + + (T ≡ bot) → + ----------- + Warningᴱ(D) + + app₁ : ∀ {M N T U Δ₁ Δ₂} {D₁ : Σ ▷ Γ ⊢ᴱ (U ⇒ S) ∋ M ∈ T ⊣ Δ₁} {D₂ : Σ ▷ Γ ⊢ᴱ (src T) ∋ N ∈ U ⊣ Δ₂} → + + Warningᴱ D₁ → + ----------------- + Warningᴱ(app D₁ D₂) + + block : ∀ b {B T Δ} {D : Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ} → + + Warningᴮ D → + ----------------- + Warningᴱ(block b D) + +data Warningᴮ {Σ Γ S} where + + return : ∀ {M B T U Δ₁ Δ₂} {D₁ : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁} {D₂ : Σ ▷ Γ ⊢ᴮ top ∋ B ∈ U ⊣ Δ₂} → + + Warningᴱ(D₁) → + ------------------ + Warningᴮ(return D₁ D₂) + + local₁ : ∀ {x M B T U V Δ₁ Δ₂} {D₁ : Σ ▷ Γ ⊢ᴱ T ∋ M ∈ U ⊣ Δ₁} {D₂ : Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂} → + + Warningᴱ(D₁) → + -------------------- + Warningᴮ(local D₁ D₂) diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda index 60de2d1b..8b12085a 100644 --- a/prototyping/Luau/Type.agda +++ b/prototyping/Luau/Type.agda @@ -5,24 +5,33 @@ open import FFI.Data.Maybe using (Maybe; just; nothing) data Type : Set where nil : Type _⇒_ : Type → Type → Type - none : Type - any : Type + bot : Type + top : Type _∪_ : Type → Type → Type _∩_ : Type → Type → Type -src : Type → Type -src nil = none -src (S ⇒ T) = S -src none = none -src any = any -src (S ∪ T) = (src S) ∪ (src T) -src (S ∩ T) = (src S) ∩ (src T) +data Mode : Set where + strict : Mode + nonstrict : Mode + +src : Mode → Type → Type +src m nil = bot +src m (S ⇒ T) = S +-- In nonstrict mode, functions are covaraiant, in strict mode they're contravariant +src strict (S ∪ T) = (src strict S) ∩ (src strict T) +src nonstrict (S ∪ T) = (src nonstrict S) ∪ (src nonstrict T) +src strict (S ∩ T) = (src strict S) ∪ (src strict T) +src nonstrict (S ∩ T) = (src nonstrict S) ∩ (src nonstrict T) +src strict bot = top +src nonstrict bot = bot +src strict top = bot +src nonstrict top = top tgt : Type → Type -tgt nil = none +tgt nil = bot tgt (S ⇒ T) = T -tgt none = none -tgt any = any +tgt bot = bot +tgt top = top tgt (S ∪ T) = (tgt S) ∪ (tgt T) tgt (S ∩ T) = (tgt S) ∩ (tgt T) diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda index 7533a3d7..5c9117ee 100644 --- a/prototyping/Luau/Type/ToString.agda +++ b/prototyping/Luau/Type/ToString.agda @@ -1,7 +1,7 @@ module Luau.Type.ToString where open import FFI.Data.String using (String; _++_) -open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_; normalizeOptional) +open import Luau.Type using (Type; nil; _⇒_; bot; top; _∪_; _∩_; normalizeOptional) {-# TERMINATING #-} typeToString : Type → String @@ -10,8 +10,8 @@ typeToStringᴵ : Type → String typeToString nil = "nil" typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T) -typeToString none = "none" -typeToString any = "any" +typeToString bot = "bot" +typeToString top = "top" typeToString (S ∪ T) with normalizeOptional(S ∪ T) typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?" typeToString (S ∪ T) | (S′ ∪ nil) = "(" ++ typeToString S′ ++ "?" diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index 8818851a..b94592c4 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -1,4 +1,6 @@ -module Luau.TypeCheck where +open import Luau.Type using (Mode) + +module Luau.TypeCheck (m : Mode) where open import Agda.Builtin.Equality using (_≡_) open import FFI.Data.Maybe using (Maybe; just) @@ -7,12 +9,15 @@ open import Luau.Var using (Var) open import Luau.Addr using (Addr) open import Luau.Heap using (Heap; HeapValue; function_is_end) renaming (_[_] to _[_]ᴴ) open import Luau.Value using (addr; val) -open import Luau.Type using (Type; nil; any; _⇒_; src; tgt) +open import Luau.Type using (Type; Mode; nil; bot; top; _⇒_; tgt) open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ) open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ) open import FFI.Data.Vector using (Vector) open import FFI.Data.Maybe using (Maybe; just; nothing) +src : Type → Type +src = Luau.Type.src m + data _▷_⊢ᴮ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Block yes → Type → VarCtxt → Set data _▷_⊢ᴱ_∋_∈_⊣_ : AddrCtxt → VarCtxt → Type → Expr yes → Type → VarCtxt → Set @@ -23,11 +28,12 @@ data _▷_⊢ᴮ_∋_∈_⊣_ where ---------------------- Σ ▷ Γ ⊢ᴮ S ∋ done ∈ nil ⊣ ∅ - return : ∀ {Σ M B S T Γ Δ} → + return : ∀ {Σ M B S T U Γ Δ₁ Δ₂} → - Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ → + Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ₁ → + Σ ▷ Γ ⊢ᴮ top ∋ B ∈ U ⊣ Δ₂ → --------------------------------- - Σ ▷ Γ ⊢ᴮ S ∋ return M ∙ B ∈ T ⊣ Δ + Σ ▷ Γ ⊢ᴮ S ∋ return M ∙ B ∈ T ⊣ Δ₁ local : ∀ {Σ x M B S T U V Γ Δ₁ Δ₂} → @@ -75,7 +81,7 @@ data _▷_⊢ᴱ_∋_∈_⊣_ where ----------------------------------------------------------------------- Σ ▷ Γ ⊢ᴱ S ∋ (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) ⊣ (Δ ⊝ x) - block : ∀ {Σ b B S T Γ Δ} → + block : ∀ b {Σ B S T Γ Δ} → Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ → ---------------------------------------------------- @@ -83,10 +89,10 @@ data _▷_⊢ᴱ_∋_∈_⊣_ where data _▷_∈_ (Σ : AddrCtxt) : Maybe (HeapValue yes) → Type → Set where - nothing : ∀ {T} → + nothing : - --------------- - Σ ▷ nothing ∈ T + ----------------- + Σ ▷ nothing ∈ bot function : ∀ {f x B T U V W} → @@ -94,6 +100,5 @@ data _▷_∈_ (Σ : AddrCtxt) : Maybe (HeapValue yes) → Type → Set where --------------------------------------------------------- Σ ▷ just (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) -data _▷_✓ (Σ : AddrCtxt) (H : Heap yes) : Set where - - defn : (∀ a → Σ ▷ (H [ a ]ᴴ) ∈ (Σ [ a ]ᴬ)) → (Σ ▷ H ✓) +_▷_✓ : AddrCtxt → Heap yes → Set +(Σ ▷ H ✓) = (∀ a → Σ ▷ (H [ a ]ᴴ) ∈ (Σ [ a ]ᴬ)) diff --git a/prototyping/Luau/VarCtxt.agda b/prototyping/Luau/VarCtxt.agda index 04a2718c..1cbcb48e 100644 --- a/prototyping/Luau/VarCtxt.agda +++ b/prototyping/Luau/VarCtxt.agda @@ -1,15 +1,15 @@ module Luau.VarCtxt where open import Agda.Builtin.Equality using (_≡_) -open import Luau.Type using (Type; none; _∪_; _∩_) +open import Luau.Type using (Type; bot; _∪_; _∩_) 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.Aeson using (KeyMap; Key; empty; unionWith; singleton; insert; delete; lookup; fromString; lookup-insert; lookup-empty) 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 +orBot : Maybe Type → Type +orBot nothing = bot +orBot (just T) = T VarCtxt : Set VarCtxt = KeyMap Type @@ -24,7 +24,7 @@ _⋓_ : VarCtxt → VarCtxt → VarCtxt _⋓_ = unionWith _∪_ _[_] : VarCtxt → Var → Type -_[_] Γ x = orNone (lookup (fromString x) Γ) +_[_] Γ x = orBot (lookup (fromString x) Γ) _⊝_ : VarCtxt → Var → VarCtxt Γ ⊝ x = delete (fromString x) Γ @@ -36,4 +36,8 @@ _⊕_↦_ : VarCtxt → Var → Type → VarCtxt Γ ⊕ x ↦ T = insert (fromString x) T Γ -- ⊕-[] : ∀ (Γ : VarCtxt) x T → (((Γ ⊕ x ↦ T) [ x ]) ≡ T) -⊕-[] = λ (Γ : VarCtxt) x T → cong orNone (lookup-insert (fromString x) T Γ) +⊕-[] = λ (Γ : VarCtxt) x T → cong orBot (lookup-insert (fromString x) T Γ) + +-- ∅-[] : ∀ x → ∅ [ x ] ≡ bot +∅-[] = λ (x : Var) → cong orBot (lookup-empty (fromString x)) + diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda index 46feee6e..1d2a54cc 100644 --- a/prototyping/Properties.agda +++ b/prototyping/Properties.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --rewriting #-} + module Properties where import Properties.Contradiction @@ -5,5 +7,7 @@ import Properties.Dec import Properties.Equality import Properties.Remember import Properties.Step +import Properties.StrictMode import Properties.TypeCheck + diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda new file mode 100644 index 00000000..fd115f56 --- /dev/null +++ b/prototyping/Properties/StrictMode.agda @@ -0,0 +1,75 @@ +{-# OPTIONS --rewriting #-} + +module Properties.StrictMode where + +import Agda.Builtin.Equality.Rewrite +open import Agda.Builtin.Equality using (_≡_; refl) +open import FFI.Data.Maybe using (Maybe; just; nothing) +open import Luau.Heap using (Heap; HeapValue; function_is_end; alloc; ok) renaming (_[_] to _[_]ᴴ) +open import Luau.StrictMode using (Warningᴱ; Warningᴮ; bot; app₁; block; return; local₁) +open import Luau.Syntax using (Expr; yes; var_∈_; _⟨_⟩∈_; _$_; addr; block_is_end; done; return; local_←_; _∙_; fun; arg) +open import Luau.Type using (Type; strict; nil; _⇒_; bot; tgt) +open import Luau.TypeCheck(strict) using (_▷_⊢ᴮ_∋_∈_⊣_; _▷_⊢ᴱ_∋_∈_⊣_; _▷_∈_; _▷_✓; nil; var; addr; app; function; block; done; return; local; nothing) +open import Luau.Value using (val; nil; addr) +open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ∅-[]) renaming (_[_] to _[_]ⱽ) +open import Properties.Remember using (remember; _,_) +open import Properties.Equality using (cong) +open import Luau.OpSem using (_⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app; function; beta; return; block; done; local; subst) + +{-# REWRITE ∅-[] #-} + +heap-miss : ∀ {Σ HV T} → (Σ ▷ HV ∈ T) → (HV ≡ nothing) → (T ≡ bot) +heap-miss nothing refl = refl + +data ProgressResultᴱ {Σ Γ S M T Δ} (H : Heap yes) (D : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) : Set +data ProgressResultᴮ {Σ Γ S B T Δ} (H : Heap yes) (D : Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) : Set + +data ProgressResultᴱ {Σ Γ S M T Δ} H D where + + value : ∀ V → (M ≡ val V) → ProgressResultᴱ H D + warning : (Warningᴱ D) → ProgressResultᴱ H D + step : ∀ {M′ H′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → ProgressResultᴱ H D + +data ProgressResultᴮ {Σ Γ S B T Δ} H D where + + done : (B ≡ done) → ProgressResultᴮ H D + return : ∀ V {C} → (B ≡ (return (val V) ∙ C)) → ProgressResultᴮ H D + warning : (Warningᴮ D) → ProgressResultᴮ H D + step : ∀ {B′ H′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → ProgressResultᴮ H D + +progressᴱ : ∀ {Σ Γ S M T Δ} H → (Σ ▷ H ✓) → (D : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → (Γ ≡ ∅) → ProgressResultᴱ H D +progressᴮ : ∀ {Σ Γ S B T Δ} H → (Σ ▷ H ✓) → (D : Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) → (Γ ≡ ∅) → ProgressResultᴮ H D + +progressᴱ H h nil _ = value nil refl +progressᴱ H h (var x p) refl = warning (bot p) +progressᴱ H h (addr a refl) _ = value (addr a) refl +progressᴱ H h (app D₁ D₂) p with progressᴱ H h D₁ p +progressᴱ H h (app nil D₂) p | value nil refl = warning (bot refl) +progressᴱ H h (app (var _ _) D₂) p | value nil () +progressᴱ H h (app (app _ _) D₂) p | value nil () +progressᴱ H h (app (function _) D₂) p | value nil () +progressᴱ H h (app (block _ _) D₂) p | value nil () +progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl with remember(H [ a ]ᴴ) +progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl | (nothing , r) = warning (bot (cong tgt (heap-miss (h a) r))) +progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl | (just(function f ⟨ var x ∈ S ⟩∈ T is B end) , r) = step (beta r) +progressᴱ H h (app D₁ D₂) p | warning W = warning (app₁ W) +progressᴱ H h (app D₁ D₂) p | step S = step (app S) +progressᴱ H h (function D) _ with alloc H _ +progressᴱ H h (function D) _ | ok a H′ r = step (function r) +progressᴱ H h (block b D) q with progressᴮ H h D q +progressᴱ H h (block b D) q | done refl = step done +progressᴱ H h (block b D) q | return V refl = step return +progressᴱ H h (block b D) q | warning W = warning (block b W) +progressᴱ H h (block b D) q | step S = step (block S) + +progressᴮ H h done q = done refl +progressᴮ H h (return D₁ D₂) q with progressᴱ H h D₁ q +progressᴮ H h (return D₁ D₂) q | value V refl = return V refl +progressᴮ H h (return D₁ D₂) q | warning W = warning (return W) +progressᴮ H h (return D₁ D₂) q | step S = step (return S) +progressᴮ H h (local D₁ D₂) q with progressᴱ H h D₁ q +progressᴮ H h (local D₁ D₂) q | value V refl = step subst +progressᴮ H h (local D₁ D₂) q | warning W = warning (local₁ W) +progressᴮ H h (local D₁ D₂) q | step S = step (local S) +progressᴮ H h (function D₁ D₂) q with alloc H _ +progressᴮ H h (function D₁ D₂) q | ok a H′ r = step (function r) diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index fbbbce69..4df8fa57 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -1,11 +1,13 @@ -module Properties.TypeCheck where +open import Luau.Type using (Mode) + +module Properties.TypeCheck (m : Mode) 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; function; block; done; return; local) +open import Luau.TypeCheck(m) 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.Type using (Type; nil; top; _⇒_; tgt) open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_; ⊕-[]) renaming (_[_] to _[_]ⱽ) open import Luau.Addr using (Addr) open import Luau.Var using (Var; _≡ⱽ_) @@ -14,6 +16,9 @@ open import Properties.Dec using (yes; no) open import Properties.Equality using (_≢_; sym; trans; cong) open import Properties.Remember using (remember; _,_) +src : Type → Type +src = Luau.Type.src m + typeOfᴱ : AddrCtxt → VarCtxt → (Expr yes) → Type typeOfᴮ : AddrCtxt → VarCtxt → (Block yes) → Type @@ -51,12 +56,12 @@ typeCheckᴱ Σ Γ S (M $ N) | ok Δ₁ D₁ | ok Δ₂ D₂ = ok (Δ₁ ⋒ Δ 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 block b is B end | ok Δ D = ok Δ (block b D) 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 (return M ∙ B) with typeCheckᴱ Σ Γ S M | typeCheckᴮ Σ Γ top B +typeCheckᴮ Σ Γ S (return M ∙ B) | ok Δ₁ D₁ | ok Σ₂ D₂ = ok Δ₁ (return D₁ D₂) typeCheckᴮ Σ Γ S done = ok ∅ done