mirror of
https://github.com/luau-lang/luau.git
synced 2025-05-04 10:33:46 +01:00
fix up strict mode typechecks
This commit is contained in:
Lily Brown
parent
d700c08e9d
commit
84ab49eb08
6 changed files with 42 additions and 10 deletions
|
|
@ -13,6 +13,7 @@ data Type : Set where
|
|||
any : Type
|
||||
boolean : Type
|
||||
number : Type
|
||||
string : Type
|
||||
_∪_ : Type → Type → Type
|
||||
_∩_ : Type → Type → Type
|
||||
|
||||
|
|
@ -25,6 +26,7 @@ lhs none = none
|
|||
lhs any = any
|
||||
lhs number = number
|
||||
lhs boolean = boolean
|
||||
lhs string = string
|
||||
|
||||
rhs : Type → Type
|
||||
rhs (_ ⇒ T) = T
|
||||
|
|
@ -35,6 +37,7 @@ rhs none = none
|
|||
rhs any = any
|
||||
rhs number = number
|
||||
rhs boolean = boolean
|
||||
rhs string = string
|
||||
|
||||
_≡ᵀ_ : ∀ (T U : Type) → Dec(T ≡ U)
|
||||
nil ≡ᵀ nil = yes refl
|
||||
|
|
@ -45,6 +48,14 @@ nil ≡ᵀ number = no (λ ())
|
|||
nil ≡ᵀ boolean = no (λ ())
|
||||
nil ≡ᵀ (S ∪ T) = no (λ ())
|
||||
nil ≡ᵀ (S ∩ T) = no (λ ())
|
||||
nil ≡ᵀ string = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ string = no (λ ())
|
||||
none ≡ᵀ string = no (λ ())
|
||||
any ≡ᵀ string = no (λ ())
|
||||
boolean ≡ᵀ string = no (λ ())
|
||||
number ≡ᵀ string = no (λ ())
|
||||
(S ∪ T) ≡ᵀ string = no (λ ())
|
||||
(S ∩ T) ≡ᵀ string = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ nil = no (λ ())
|
||||
(S ⇒ T) ≡ᵀ (U ⇒ V) with (S ≡ᵀ U) | (T ≡ᵀ V)
|
||||
(S ⇒ T) ≡ᵀ (S ⇒ T) | yes refl | yes refl = yes refl
|
||||
|
|
@ -88,6 +99,15 @@ boolean ≡ᵀ boolean = yes refl
|
|||
boolean ≡ᵀ number = no (λ ())
|
||||
boolean ≡ᵀ (T ∪ U) = no (λ ())
|
||||
boolean ≡ᵀ (T ∩ U) = no (λ ())
|
||||
string ≡ᵀ nil = no (λ ())
|
||||
string ≡ᵀ (x ⇒ x₁) = no (λ ())
|
||||
string ≡ᵀ none = no (λ ())
|
||||
string ≡ᵀ any = no (λ ())
|
||||
string ≡ᵀ boolean = no (λ ())
|
||||
string ≡ᵀ number = no (λ ())
|
||||
string ≡ᵀ string = yes refl
|
||||
string ≡ᵀ (U ∪ V) = no (λ ())
|
||||
string ≡ᵀ (U ∩ V) = no (λ ())
|
||||
(S ∪ T) ≡ᵀ nil = no (λ ())
|
||||
(S ∪ T) ≡ᵀ (U ⇒ V) = no (λ ())
|
||||
(S ∪ T) ≡ᵀ none = no (λ ())
|
||||
|
|
@ -127,6 +147,7 @@ src : Mode → Type → Type
|
|||
src m nil = none
|
||||
src m number = none
|
||||
src m boolean = none
|
||||
src m string = none
|
||||
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)
|
||||
|
|
@ -145,6 +166,7 @@ tgt none = none
|
|||
tgt any = any
|
||||
tgt number = none
|
||||
tgt boolean = none
|
||||
tgt string = none
|
||||
tgt (S ∪ T) = (tgt S) ∪ (tgt T)
|
||||
tgt (S ∩ T) = (tgt S) ∩ (tgt T)
|
||||
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
|
||||
module Luau.Type.FromJSON where
|
||||
|
||||
open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)
|
||||
open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number; string)
|
||||
|
||||
open import Agda.Builtin.List using (List; _∷_; [])
|
||||
open import Agda.Builtin.Bool using (true; false)
|
||||
|
|
@ -44,6 +44,7 @@ typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o
|
|||
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil
|
||||
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right any
|
||||
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "number") = Right number
|
||||
typeFromJSON (object o) | just (string "AstTypeReference") | just (string "string") = Right string
|
||||
typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"
|
||||
|
||||
typeFromJSON (object o) | just (string "AstTypeUnion") with lookup types o
|
||||
|
|
|
|||
|
|
@ -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; number; boolean; _∪_; _∩_; normalizeOptional)
|
||||
open import Luau.Type using (Type; nil; _⇒_; none; any; number; boolean; string; _∪_; _∩_; normalizeOptional)
|
||||
|
||||
{-# TERMINATING #-}
|
||||
typeToString : Type → String
|
||||
|
|
@ -14,6 +14,7 @@ typeToString none = "none"
|
|||
typeToString any = "any"
|
||||
typeToString number = "number"
|
||||
typeToString boolean = "boolean"
|
||||
typeToString string = "string"
|
||||
typeToString (S ∪ T) with normalizeOptional(S ∪ T)
|
||||
typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
|
||||
typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"
|
||||
|
|
|
|||
|
|
@ -6,11 +6,11 @@ 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; 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 _[_]ᴴ)
|
||||
open import Luau.Type using (Type; Mode; nil; none; number; boolean; _⇒_; tgt)
|
||||
open import Luau.Type using (Type; Mode; nil; none; number; boolean; string; _⇒_; tgt)
|
||||
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
|
||||
open import FFI.Data.Vector using (Vector)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
|
|
@ -93,6 +93,11 @@ data _⊢ᴱ_∈_ where
|
|||
|
||||
--------------------------
|
||||
Γ ⊢ᴱ val(bool b) ∈ boolean
|
||||
|
||||
string : ∀ {x Γ} →
|
||||
|
||||
---------------------------
|
||||
Γ ⊢ᴱ val(string x) ∈ string
|
||||
|
||||
app : ∀ {M N T U Γ} →
|
||||
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ 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.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
|
||||
open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
|
||||
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; _≡ᵀ_; _≡ᴹᵀ_)
|
||||
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orNone; tgtBinOp)
|
||||
open import Luau.Var using (_≡ⱽ_)
|
||||
|
|
@ -86,6 +86,7 @@ heap-weakeningᴱ H (val (addr a)) (snoc {a = a} defn) | yes refl = warning (Una
|
|||
heap-weakeningᴱ H (val (addr a)) (snoc {a = b} p) | no q = ok (cong orNone (cong typeOfᴹᴼ (lookup-not-allocated p q)))
|
||||
heap-weakeningᴱ H (val (number n)) h = ok refl
|
||||
heap-weakeningᴱ H (val (bool b)) h = ok refl
|
||||
heap-weakeningᴱ H (val (string x)) h = ok refl
|
||||
heap-weakeningᴱ H (binexp M op N) h = ok refl
|
||||
heap-weakeningᴱ H (M $ N) h with heap-weakeningᴱ H M h
|
||||
heap-weakeningᴱ H (M $ N) h | ok p = ok (cong tgt p)
|
||||
|
|
@ -110,6 +111,7 @@ typeOf-val-not-none : ∀ {H Γ} v → OrWarningᴱ H (typeCheckᴱ H Γ (val v)
|
|||
typeOf-val-not-none nil = ok (λ ())
|
||||
typeOf-val-not-none (number n) = ok (λ ())
|
||||
typeOf-val-not-none (bool b) = ok (λ ())
|
||||
typeOf-val-not-none (string x) = ok (λ ())
|
||||
typeOf-val-not-none {H = H} (addr a) with remember (H [ a ]ᴴ)
|
||||
typeOf-val-not-none {H = H} (addr a) | (just O , p) = ok (λ q → none-not-obj O (trans q (cong orNone (cong typeOfᴹᴼ p))))
|
||||
typeOf-val-not-none {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress p)
|
||||
|
|
|
|||
|
|
@ -8,9 +8,9 @@ open import Agda.Builtin.Equality using (_≡_; refl)
|
|||
open import Agda.Builtin.Bool using (Bool; true; false)
|
||||
open import FFI.Data.Maybe using (Maybe; just; nothing)
|
||||
open import FFI.Data.Either using (Either)
|
||||
open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; app; function; block; binexp; done; return; local; nothing; orNone; tgtBinOp)
|
||||
open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; 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; _⇒_; tgt)
|
||||
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.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
|
||||
open import Luau.Addr using (Addr)
|
||||
|
|
@ -37,6 +37,7 @@ typeOfⱽ H nil = just nil
|
|||
typeOfⱽ H (bool b) = just boolean
|
||||
typeOfⱽ H (addr a) = typeOfᴹᴼ (H [ a ]ᴴ)
|
||||
typeOfⱽ H (number n) = just number
|
||||
typeOfⱽ H (string x) = just string
|
||||
|
||||
typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type
|
||||
typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type
|
||||
|
|
@ -59,6 +60,7 @@ mustBeFunction H Γ (addr a) p = refl
|
|||
mustBeFunction H Γ (number n) p = CONTRADICTION (p refl)
|
||||
mustBeFunction H Γ (bool true) p = CONTRADICTION (p refl)
|
||||
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 ()
|
||||
|
|
@ -68,8 +70,6 @@ mustBeNumber H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B en
|
|||
mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
|
||||
mustBeNumber H Γ (addr a) p | nothing , q | ()
|
||||
mustBeNumber H Γ (number n) p = refl
|
||||
mustBeNumber H Γ (bool true) ()
|
||||
mustBeNumber H Γ (bool false) ()
|
||||
|
||||
typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M))
|
||||
typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B))
|
||||
|
|
@ -79,6 +79,7 @@ typeCheckᴱ H Γ (val nil) = nil
|
|||
typeCheckᴱ H Γ (val (addr a)) = addr (orNone (typeOfᴹᴼ (H [ a ]ᴴ)))
|
||||
typeCheckᴱ H Γ (val (number n)) = number
|
||||
typeCheckᴱ H Γ (val (bool b)) = bool
|
||||
typeCheckᴱ H Γ (val (string x)) = string
|
||||
typeCheckᴱ H Γ (M $ N) = app (typeCheckᴱ H Γ M) (typeCheckᴱ H Γ N)
|
||||
typeCheckᴱ H Γ (function f ⟨ var x ∈ T ⟩∈ U is B end) = function (typeCheckᴮ H (Γ ⊕ x ↦ T) B)
|
||||
typeCheckᴱ H Γ (block var b ∈ T is B end) = block (typeCheckᴮ H Γ B)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue