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

Fixed some processing of options

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-02-10 20:46:39 -06:00
parent 2a7cc199a9
commit 99fe8b3df9
3 changed files with 12 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
prototyping/Examples/Type.agda
View file

@ -19,3 +19,9 @@ ex4 = refl
ex5 : typeToString(nil ⇒ ((nil ⇒ nil) ∪ nil)) ≡ "(nil) -> ((nil) -> nil)?"
ex5 = refl
ex6 : typeToString((nil ⇒ nil) ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)"
ex6 = refl
ex7 : typeToString((nil ⇒ nil) ∪ ((nil ⇒ (nil ⇒ nil)) ∪ nil)) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)?"
ex7 = refl

8
prototyping/Luau/Type.agda
View file

@ -34,8 +34,10 @@ optional T = (T ∪ nil)
normalizeOptional : Type → Type
normalizeOptional (S ∪ T) with normalizeOptional S | normalizeOptional T
normalizeOptional (S ∪ T) | (S′ ∪ nil) | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
normalizeOptional (S ∪ T) | S′ | nil = optional S′
normalizeOptional (S ∪ T) | nil | T′ = optional T′
normalizeOptional (S ∪ T) | S′ | T′ = S′ ∪ T′
normalizeOptional (S ∪ T) | S′ | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
normalizeOptional (S ∪ T) | (S′ ∪ nil) | T′ = (S′ ∪ T′) ∪ nil
normalizeOptional (S ∪ T) | S′ | nil = optional S′
normalizeOptional (S ∪ T) | nil | T′ = optional T′
normalizeOptional (S ∪ T) | S′ | T′ = S′ ∪ T′
normalizeOptional T = T

4
prototyping/Luau/Type/ToString.agda
View file

@ -14,15 +14,13 @@ typeToString none = "none"
typeToString any = "any"
typeToString (S ∪ T) with normalizeOptional(S ∪ T)
typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
typeToString (S ∪ T) | (S′ ∪ nil) = "(" ++ typeToString S′ ++ "?"
typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"
typeToString (S ∪ T) | (S′ ∪ T′) = "(" ++ typeToStringᵁ (S ∪ T) ++ ")"
typeToString (S ∪ T) | T′ = typeToString T′
typeToString (S ∩ T) = "(" ++ typeToStringᴵ (S ∩ T) ++ ")"
typeToStringᵁ (S ⇒ T) = "(" ++ typeToString (S ⇒ T) ++ ")"
typeToStringᵁ (S ∪ T) = (typeToStringᵁ S) ++ " | " ++ (typeToStringᵁ T)
typeToStringᵁ T = typeToString T
typeToStringᴵ (S ⇒ T) = "(" ++ typeToString (S ⇒ T) ++ ")"
typeToStringᴵ (S ∩ T) = (typeToStringᴵ S) ++ " & " ++ (typeToStringᴵ T)
typeToStringᴵ T = typeToString T