luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

add concat operator

Browse source
This commit is contained in:
Lily Brown 2022-03-02 14:56:10 -08:00
parent 51ca4720ce
commit 48e9300571
10 changed files with 46 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
prototyping/Luau/OpSem.agda
View file

@ -5,13 +5,13 @@ module Luau.OpSem where
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess; primFloatInequality)
open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.String using (primStringEquality)
open import Agda.Builtin.String using (primStringEquality; primStringAppend)
open import Utility.Bool using (not; _or_; _and_)
open import Agda.Builtin.Nat using () renaming (_==_ to _==ᴬ_)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Syntax using (Value; Expr; Stat; Block; nil; addr; val; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; number; bool)
open import Luau.Syntax using (Value; Expr; Stat; Block; nil; addr; val; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; ··; number; bool; string)
open import Luau.RuntimeType using (RuntimeType; valueType)
open import Properties.Product using (_×_; _,_)
@ -38,6 +38,7 @@ data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where
>= : ∀ m n → (number m) ⟦ >= ⟧ (number n) ⟶ bool ((primFloatLess n m) or (primFloatEquality m n))
== : ∀ v w → v ⟦ == ⟧ w ⟶ bool (evalEqOp v w)
~= : ∀ v w → v ⟦ ~= ⟧ w ⟶ bool (evalNeqOp v w)
·· : ∀ x y → (string x) ⟦ ·· ⟧ (string y) ⟶ string (primStringAppend x y)
data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set

5
prototyping/Luau/RuntimeError.agda
View file

@ -6,8 +6,8 @@ open import Agda.Builtin.Equality using (_≡_)
open import Luau.Heap using (Heap; _[_])
open import FFI.Data.Maybe using (just; nothing)
open import FFI.Data.String using (String)
open import Luau.Syntax using (BinaryOperator; Block; Expr; nil; var; val; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp; +; -; *; /; <; >; <=; >=)
open import Luau.RuntimeType using (RuntimeType; valueType; function; number)
open import Luau.Syntax using (BinaryOperator; Block; Expr; nil; var; val; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; string; binexp; +; -; *; /; <; >; <=; >=; ··)
open import Luau.RuntimeType using (RuntimeType; valueType; function; number; string)
open import Properties.Equality using (_≢_)
data BinOpError : BinaryOperator → RuntimeType → Set where
@ -19,6 +19,7 @@ data BinOpError : BinaryOperator → RuntimeType → Set where
> : ∀ {t} → (t ≢ number) → BinOpError > t
<= : ∀ {t} → (t ≢ number) → BinOpError <= t
>= : ∀ {t} → (t ≢ number) → BinOpError >= t
·· : ∀ {t} → (t ≢ string) → BinOpError ·· t
data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set

5
prototyping/Luau/StrictMode.agda
View file

@ -4,8 +4,8 @@ module Luau.StrictMode where
open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=)
open import Luau.Type using (Type; strict; nil; number; _⇒_; tgt)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
open import Luau.Type using (Type; strict; nil; number; string; _⇒_; tgt)
open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function)
@ -25,6 +25,7 @@ data BinOpWarning : BinaryOperator → Type → Set where
> : ∀ {T} → (T ≢ number) → BinOpWarning > T
<= : ∀ {T} → (T ≢ number) → BinOpWarning <= T
>= : ∀ {T} → (T ≢ number) → BinOpWarning >= T
·· : ∀ {T} → (T ≢ string) → BinOpWarning ·· T
data Warningᴱ (H : Heap yes) {Γ} : ∀ {M T} → (Γ ⊢ᴱ M ∈ T) → Set
data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set

1
prototyping/Luau/Syntax.agda
View file

@ -46,6 +46,7 @@ data BinaryOperator : Set where
~= : BinaryOperator
<= : BinaryOperator
>= : BinaryOperator
·· : BinaryOperator
data Value : Set where
nil : Value

3
prototyping/Luau/Syntax/FromJSON.agda
View file

@ -2,7 +2,7 @@
module Luau.Syntax.FromJSON where
open import Luau.Syntax using (Block; Stat ; Expr; _$_; val; nil; bool; number; var; var_∈_; function_is_end; _⟨_⟩; _⟨_⟩∈_; local_←_; return; done; _∙_; maybe; VarDec; binexp; BinaryOperator; +; -; *; /; ==; ~=; <; >; <=; >=; string)
open import Luau.Syntax using (Block; Stat ; Expr; _$_; val; nil; bool; number; var; var_∈_; function_is_end; _⟨_⟩; _⟨_⟩∈_; local_←_; return; done; _∙_; maybe; VarDec; binexp; BinaryOperator; +; -; *; /; ==; ~=; <; >; <=; >=; ··; string)
open import Luau.Type.FromJSON using (typeFromJSON)
open import Agda.Builtin.List using (List; _∷_; [])
@ -65,6 +65,7 @@ binOpFromString "CompareLt" = Right <
binOpFromString "CompareLe" = Right <=
binOpFromString "CompareGt" = Right >
binOpFromString "CompareGe" = Right >=
binOpFromString "Concat" = Right ··
binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
varDecFromJSON (object arg) = varDecFromObject arg

3
prototyping/Luau/Syntax/ToString.agda
View file

@ -3,7 +3,7 @@ module Luau.Syntax.ToString where
open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Float using (primShowFloat)
open import Agda.Builtin.String using (primShowString)
open import Luau.Syntax using (Value; Block; Stat; Expr; VarDec; FunDec; nil; bool; val; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; binexp; string)
open import Luau.Syntax using (Value; Block; Stat; Expr; VarDec; FunDec; nil; bool; val; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ==; ~=; <=; >=; ··; binexp; string)
open import FFI.Data.String using (String; _++_)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Type.ToString using (typeToString)
@ -30,6 +30,7 @@ binOpToString == = "=="
binOpToString ~= = "~="
binOpToString <= = "<="
binOpToString >= = ">="
binOpToString ·· = ".."
valueToString : Value → String
valueToString nil = "nil"

3
prototyping/Luau/TypeCheck.agda
View file

@ -6,7 +6,7 @@ module Luau.TypeCheck (m : Mode) where
open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (Maybe; just)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; string; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; string; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
open import Luau.Var using (Var)
open import Luau.Addr using (Addr)
open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
@ -34,6 +34,7 @@ tgtBinOp == = boolean
tgtBinOp ~= = boolean
tgtBinOp <= = boolean
tgtBinOp >= = boolean
tgtBinOp ·· = string
data _⊢ᴮ_∈_ : VarCtxt → Block yes → Type → Set
data _⊢ᴱ_∈_ : VarCtxt → Expr yes → Type → Set

17
prototyping/Properties/Step.agda
View file

@ -5,11 +5,12 @@ module Properties.Step where
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess)
open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.String using (primStringAppend)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
open import Luau.Syntax using (Block; Expr; nil; var; val; addr; bool; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; -; *; /; <; >; <=; >=; ==; ~=; string)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOp₀; binOp₁; binOp₂; +; -; *; /; <; >; <=; >=; ==; ~=; evalEqOp; evalNeqOp)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂; +; -; *; /; <; >; <=; >=)
open import Luau.Syntax using (Block; Expr; nil; var; val; addr; bool; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; -; *; /; <; >; <=; >=; ==; ~=; ··; string)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOp₀; binOp₁; binOp₂; +; -; *; /; <; >; <=; >=; ==; ~=; ··; evalEqOp; evalNeqOp)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂; +; -; *; /; <; >; <=; >=; ··)
open import Luau.RuntimeType using (valueType; function; number)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Properties.Remember using (remember; _,_)
@ -97,6 +98,15 @@ binOpStep (string x) < w = error₁ (< (λ ()))
binOpStep (string x) > w = error₁ (> (λ ()))
binOpStep (string x) <= w = error₁ (<= (λ ()))
binOpStep (string x) >= w = error₁ (>= (λ ()))
binOpStep nil ·· y = error₁ (·· (λ ()))
binOpStep (addr x) ·· y = error₁ (BinOpError.·· (λ ()))
binOpStep (number x) ·· y = error₁ (BinOpError.·· (λ ()))
binOpStep (bool x) ·· y = error₁ (BinOpError.·· (λ ()))
binOpStep (string x) ·· nil = error₂ (·· (λ ()))
binOpStep (string x) ·· (addr y) = error₂ (·· (λ ()))
binOpStep (string x) ·· (number y) = error₂ (·· (λ ()))
binOpStep (string x) ·· (bool y) = error₂ (·· (λ ()))
binOpStep (string x) ·· (string y) = step (string (primStringAppend x y)) (·· x y)
data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set
@ -159,3 +169,4 @@ stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (r
stepᴮ H (return _ ∙ B) | value V refl = return V refl
stepᴮ H (return M ∙ B) | error E = error (return E)
stepᴮ H done = done refl

10
prototyping/Properties/StrictMode.agda
View file

@ -6,7 +6,7 @@ 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; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ)
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpWarning; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr; +; -; *; /; <; >; <=; >=)
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpWarning; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr; +; -; *; /; <; >; <=; >=; ··)
open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
open import Luau.Type using (Type; strict; nil; _⇒_; none; tgt; _≡ᵀ_; _≡ᴹᵀ_)
@ -19,9 +19,9 @@ open import Properties.Remember using (remember; _,_)
open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
open import Properties.Dec using (Dec; yes; no)
open import Properties.Contradiction using (CONTRADICTION)
open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=)
open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber; mustBeString)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)
open import Luau.RuntimeType using (valueType)
src = Luau.Type.src strict
@ -155,6 +155,7 @@ binOpPreservation H (<= m n) = refl
binOpPreservation H (>= m n) = refl
binOpPreservation H (== v w) = refl
binOpPreservation H (~= v w) = refl
binOpPreservation H (·· v w) = refl
preservationᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H ∅ M) (typeOfᴱ H ∅ M ≡ typeOfᴱ H′ ∅ M′)
preservationᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H ∅ B) (typeOfᴮ H ∅ B ≡ typeOfᴮ H′ ∅ B′)
@ -446,6 +447,7 @@ runtimeBinOpWarning H v (< p) = < (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (> p) = > (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (<= p) = <= (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (>= p) = >= (λ q → p (mustBeNumber H ∅ v q))
runtimeBinOpWarning H v (·· p) = ·· (λ q → p (mustBeString H ∅ v q))
runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M)
runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B)

12
prototyping/Properties/TypeCheck.agda
View file

@ -11,7 +11,7 @@ open import FFI.Data.Either using (Either)
open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orNone; tgtBinOp)
open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
open import Luau.Type using (Type; nil; any; none; number; boolean; string; _⇒_; tgt)
open import Luau.RuntimeType using (RuntimeType; nil; number; function; valueType)
open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType)
open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import Luau.Addr using (Addr)
open import Luau.Var using (Var; _≡ⱽ_)
@ -63,7 +63,6 @@ mustBeFunction H Γ (bool false) p = CONTRADICTION (p refl)
mustBeFunction H Γ (string x) p = CONTRADICTION (p refl)
mustBeNumber : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ number) → (valueType(v) ≡ number)
mustBeNumber H Γ nil ()
mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ)
mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
mustBeNumber H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
@ -71,6 +70,14 @@ mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeO
mustBeNumber H Γ (addr a) p | nothing , q | ()
mustBeNumber H Γ (number n) p = refl
mustBeString : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ string) → (valueType(v) ≡ string)
mustBeString H Γ (addr a) p with remember (H [ a ]ᴴ)
mustBeString H Γ (addr a) p | (just O , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
mustBeString H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
mustBeString H Γ (addr a) p | (nothing , q) | ()
mustBeString H Γ (string x) p = refl
typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M))
typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B))
@ -102,3 +109,4 @@ typeCheckᴴᴱ H Γ M = (typeCheckᴴ H , typeCheckᴱ H Γ M)
typeCheckᴴᴮ : ∀ H Γ M → (Γ ⊢ᴴᴮ H ▷ M ∈ typeOfᴮ H Γ M)
typeCheckᴴᴮ H Γ M = (typeCheckᴴ H , typeCheckᴮ H Γ M)