From 4033100f50bdbf816fbfd57ed853b2c4129d5935 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Tue, 26 Apr 2022 13:35:12 -0500 Subject: [PATCH] WIP --- prototyping/Luau/TypeNormalization.agda | 2 +- prototyping/Properties/TypeNormalization.agda | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/prototyping/Luau/TypeNormalization.agda b/prototyping/Luau/TypeNormalization.agda index ba4a00ba..341883ea 100644 --- a/prototyping/Luau/TypeNormalization.agda +++ b/prototyping/Luau/TypeNormalization.agda @@ -25,7 +25,7 @@ S ∪ⁿ unknown = unknown S ∪ⁿ never = S unknown ∪ⁿ T = unknown never ∪ⁿ T = T -(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂ +(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂ F ∪ⁿ G = F ∪ᶠ G -- Intersection of normalized types diff --git a/prototyping/Properties/TypeNormalization.agda b/prototyping/Properties/TypeNormalization.agda index 4b069b47..299f648c 100644 --- a/prototyping/Properties/TypeNormalization.agda +++ b/prototyping/Properties/TypeNormalization.agda @@ -16,7 +16,7 @@ data FunType where _⇒_ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ T) _∩_ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ G) -data Normal where +data Normal where never : Normal never unknown : Normal unknown _⇒_ : ∀ {S T} → Normal S → Normal T → Normal (S ⇒ T) @@ -29,7 +29,7 @@ data OptScalar : Type → Set where boolean : OptScalar boolean string : OptScalar string nil : OptScalar nil - + -- Normalization produces normal types normal : ∀ T → Normal (normalize T) normalᶠ : ∀ {F} → FunType F → Normal F @@ -60,7 +60,7 @@ normal-∪ⁿ never (G₁ ∩ G₂) = G₁ ∩ G₂ normal-∪ⁿ unknown (T ⇒ U) = unknown normal-∪ⁿ unknown (G₁ ∩ G₂) = unknown 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₂) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (G₁ ∩ G₂)) normal-∪ⁿ (S₁ ∪ S₂) (T₁ ⇒ T₂) = normal-∪ⁿ S₁ (T₁ ⇒ T₂) ∪ S₂