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

WIP

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-05-12 19:11:13 -05:00
parent b1b1fffbbd
commit b76621d21a
3 changed files with 26 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
prototyping/Luau/TypeNormalization.agda
View file

@ -9,6 +9,7 @@ _∩ⁿˢ_ : Type → Type → Type
_∪ⁿ_ : Type → Type → Type _∪ⁿ_ : Type → Type → Type
_∩ⁿ_ : Type → Type → Type _∩ⁿ_ : Type → Type → Type
_⇒ⁿ_ : Type → Type → Type _⇒ⁿ_ : Type → Type → Type
tgtⁿ : Type → Type → Type
-- Union of function types -- Union of function types
(F₁ ∩ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) ∩ (F₂ ∪ᶠ G) (F₁ ∩ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) ∩ (F₂ ∪ᶠ G)
@ -54,8 +55,10 @@ unknown ∪ⁿˢ T = unknown
F ∪ⁿˢ T = F ∪ T F ∪ⁿˢ T = F ∪ T
-- Functions on normalized types -- Functions on normalized types
never ⇒ⁿ T = never ⇒ unknown S ⇒ⁿ T = S ⇒ (tgtⁿ S T)
S ⇒ⁿ T = S ⇒ T
tgtⁿ never T = unknown
tgtⁿ S T = T
-- Normalize! -- Normalize!
normalize : Type → Type normalize : Type → Type

9
prototyping/Properties/Subtyping.agda
View file

@ -165,6 +165,12 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
<:-∩-symm : ∀ {T U} → (T ∩ U) <: (U ∩ T) <:-∩-symm : ∀ {T U} → (T ∩ U) <: (U ∩ T)
<:-∩-symm t (p₁ , p₂) = (p₂ , p₁) <:-∩-symm t (p₁ , p₂) = (p₂ , p₁)
<:-∩-assocl : ∀ {S T U} → (S ∩ (T ∩ U)) <: ((S ∩ T) ∩ U)
<:-∩-assocl t (p , (p₁ , p₂)) = (p , p₁) , p₂
<:-∩-assocr : ∀ {S T U} → ((S ∩ T) ∩ U) <: (S ∩ (T ∩ U))
<:-∩-assocr t ((p , p₁) , p₂) = p , (p₁ , p₂)
≮:-∩-left : ∀ {S T U} → (S ≮: T) → (S ≮: (T ∩ U)) ≮:-∩-left : ∀ {S T U} → (S ≮: T) → (S ≮: (T ∩ U))
≮:-∩-left (witness t p q) = witness t p (left q) ≮:-∩-left (witness t p q) = witness t p (left q)
@ -206,6 +212,9 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
∪-distr-∩-<: t (left p₁ , right p₂) = right p₂ ∪-distr-∩-<: t (left p₁ , right p₂) = right p₂
∪-distr-∩-<: t (right p₁ , p₂) = right p₁ ∪-distr-∩-<: t (right p₁ , p₂) = right p₁
∩-<:-∪ : ∀ {S T} → (S ∩ T) <: (S ∪ T)
∩-<:-∪ t (p , _) = left p
-- Properties of functions -- Properties of functions
<:-function : ∀ {R S T U} → (R <: S) → (T <: U) → (S ⇒ T) <: (R ⇒ U) <:-function : ∀ {R S T U} → (R <: S) → (T <: U) → (S ⇒ T) <: (R ⇒ U)
<:-function p q function function = function <:-function p q function function = function

13
prototyping/Properties/TypeNormalization.agda
View file

@ -4,7 +4,7 @@ module Properties.TypeNormalization where
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_) open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
open import Luau.Subtyping using (Tree; Language; function; scalar; unknown; right; scalar-function-err; _,_) open import Luau.Subtyping using (Tree; Language; function; scalar; unknown; right; scalar-function-err; _,_)
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; _⇒ⁿ_; normalize) open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; _⇒ⁿ_; tgtⁿ; normalize)
open import Luau.Subtyping using (_<:_) open import Luau.Subtyping using (_<:_)
open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∩-symm; <:-function; <:-function-∪-∩; <:-function-∩-∪; <:-function-∪; <:-everything; <:-union; <:-∪-assocl; <:-∪-assocr; <:-∪-symm; <:-intersect; ∪-distl-∩-<:; ∪-distr-∩-<:; <:-∪-distr-∩; <:-∪-distl-∩; ∩-distl-∪-<:; <:-∩-distl-∪; <:-∩-distr-∪; scalar-∩-function-<:-never; scalar-≢-∩-<:-never; <:-function-never) open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∩-symm; <:-function; <:-function-∪-∩; <:-function-∩-∪; <:-function-∪; <:-everything; <:-union; <:-∪-assocl; <:-∪-assocr; <:-∪-symm; <:-intersect; ∪-distl-∩-<:; ∪-distr-∩-<:; <:-∪-distr-∩; <:-∪-distl-∩; ∩-distl-∪-<:; <:-∩-distl-∪; <:-∩-distr-∪; scalar-∩-function-<:-never; scalar-≢-∩-<:-never; <:-function-never)
@ -237,6 +237,17 @@ scalar-∩-fun-<:-never function S = scalar-∩-function-<:-never S
scalar-∩-fun-<:-never (T ⇒ U) S = scalar-∩-function-<:-never S scalar-∩-fun-<:-never (T ⇒ U) S = scalar-∩-function-<:-never S
scalar-∩-fun-<:-never (F ∩ G) S = <:-trans (<:-intersect <:-∩-left <:-refl) (scalar-∩-fun-<:-never F S) scalar-∩-fun-<:-never (F ∩ G) S = <:-trans (<:-intersect <:-∩-left <:-refl) (scalar-∩-fun-<:-never F S)
<:-tgtⁿ : ∀ {S T U} → (T <: U) → T <: tgtⁿ S U
<:-tgtⁿ {never} p = <:-unknown
<:-tgtⁿ {nil} p = p
<:-tgtⁿ {unknown} p = p
<:-tgtⁿ {boolean} p = p
<:-tgtⁿ {number} p = p
<:-tgtⁿ {string} p = p
<:-tgtⁿ {S ⇒ T} p = p
<:-tgtⁿ {S ∪ T} p = p
<:-tgtⁿ {S ∩ T} p = p
flipper : ∀ {S T U} → ((S ∪ T) ∪ U) <: ((S ∪ U) ∪ T) flipper : ∀ {S T U} → ((S ∪ T) ∪ U) <: ((S ∪ U) ∪ T)
flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪-assocl) flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪-assocl)