From 1733f300bbbf51819b3ee5133dba6ad8d894d100 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Fri, 22 Apr 2022 19:11:57 -0500 Subject: [PATCH] WIP --- prototyping/Luau/TypeNormalization.agda | 26 +++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/prototyping/Luau/TypeNormalization.agda b/prototyping/Luau/TypeNormalization.agda index bb982eed..5702d907 100644 --- a/prototyping/Luau/TypeNormalization.agda +++ b/prototyping/Luau/TypeNormalization.agda @@ -6,8 +6,7 @@ open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; ¬function : Type ¬function = number ∪ (string ∪ (nil ∪ boolean)) --- Normalize -normalize : Type → Type +-- Unions and intersections of normalized types _∪ᶠ_ : Type → Type → Type _∩ᶠ_ : Type → Type → Type _∪ⁿˢ_ : Type → Type → Type @@ -16,16 +15,6 @@ _∪ⁿ_ : Type → Type → Type _∩ⁿ_ : Type → Type → Type _⇒ᶠ_ : Type → Type → Type -normalize nil = never ∪ nil -normalize (S ⇒ T) = (normalize S ⇒ᶠ normalize T) -normalize never = never -normalize unknown = unknown -normalize boolean = never ∪ boolean -normalize number = never ∪ number -normalize string = never ∪ string -normalize (S ∪ T) = normalize S ∪ⁿ normalize T -normalize (S ∩ T) = normalize S ∩ⁿ normalize T - -- Union of function types never ∪ᶠ G = G F ∪ᶠ never = F @@ -76,3 +65,16 @@ F ∪ⁿˢ T = F ∪ T -- Functions between normalized types (never ⇒ᶠ T) = (never ⇒ unknown) (S ⇒ᶠ T) = (S ⇒ T) + +-- Normalize! +normalize : Type → Type +normalize nil = never ∪ nil +normalize (S ⇒ T) = (normalize S ⇒ᶠ normalize T) +normalize never = never +normalize unknown = unknown +normalize boolean = never ∪ boolean +normalize number = never ∪ number +normalize string = never ∪ string +normalize (S ∪ T) = normalize S ∪ⁿ normalize T +normalize (S ∩ T) = normalize S ∩ⁿ normalize T +