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-04-26 13:35:12 -05:00
parent 658fce4631
commit 4033100f50
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
prototyping/Luau/TypeNormalization.agda
View file

@ -25,7 +25,7 @@ S ∪ⁿ unknown = unknown
S ∪ⁿ never = S S ∪ⁿ never = S
unknown ∪ⁿ T = unknown unknown ∪ⁿ T = unknown
never ∪ⁿ T = T never ∪ⁿ T = T
(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂ (S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂
F ∪ⁿ G = F ∪ᶠ G F ∪ⁿ G = F ∪ᶠ G
-- Intersection of normalized types -- Intersection of normalized types

6
prototyping/Properties/TypeNormalization.agda
View file

@ -16,7 +16,7 @@ data FunType where
_⇒_ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ T) _⇒_ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ T)
_∩_ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ G) _∩_ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ G)
data Normal where data Normal where
never : Normal never never : Normal never
unknown : Normal unknown unknown : Normal unknown
_⇒_ : ∀ {S T} → Normal S → Normal T → Normal (S ⇒ T) _⇒_ : ∀ {S T} → Normal S → Normal T → Normal (S ⇒ T)
@ -29,7 +29,7 @@ data OptScalar : Type → Set where
boolean : OptScalar boolean boolean : OptScalar boolean
string : OptScalar string string : OptScalar string
nil : OptScalar nil nil : OptScalar nil
-- Normalization produces normal types -- Normalization produces normal types
normal : ∀ T → Normal (normalize T) normal : ∀ T → Normal (normalize T)
normalᶠ : ∀ {F} → FunType F → Normal F normalᶠ : ∀ {F} → FunType F → Normal F
@ -60,7 +60,7 @@ normal-∪ⁿ never (G₁ ∩ G₂) = G₁ ∩ G₂
normal-∪ⁿ unknown (T ⇒ U) = unknown normal-∪ⁿ unknown (T ⇒ U) = unknown
normal-∪ⁿ unknown (G₁ ∩ G₂) = unknown normal-∪ⁿ unknown (G₁ ∩ G₂) = unknown
normal-∪ⁿ (R ⇒ S) (T ⇒ U) = normalᶠ (normal-∪ᶠ (R ⇒ S) (T ⇒ U)) normal-∪ⁿ (R ⇒ S) (T ⇒ U) = normalᶠ (normal-∪ᶠ (R ⇒ S) (T ⇒ U))
normal-∪ⁿ (R ⇒ S) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (R ⇒ S) (G₁ ∩ G₂)) normal-∪ⁿ (R ⇒ S) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (R ⇒ S) (G₁ ∩ G₂))
normal-∪ⁿ (F₁ ∩ F₂) (T ⇒ U) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (T ⇒ U)) normal-∪ⁿ (F₁ ∩ F₂) (T ⇒ U) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (T ⇒ U))
normal-∪ⁿ (F₁ ∩ F₂) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (G₁ ∩ G₂)) normal-∪ⁿ (F₁ ∩ F₂) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (G₁ ∩ G₂))
normal-∪ⁿ (S₁ ∪ S₂) (T₁ ⇒ T₂) = normal-∪ⁿ S₁ (T₁ ⇒ T₂) ∪ S₂ normal-∪ⁿ (S₁ ∪ S₂) (T₁ ⇒ T₂) = normal-∪ⁿ S₁ (T₁ ⇒ T₂) ∪ S₂