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-02-24 11:34:11 -06:00
parent 02f5e21331
commit 9f6fc4a56b
2 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
prototyping/Examples/Type.agda
View file

@ -1,5 +1,3 @@
{-# OPTIONS --allow-unsolved-metas #-}
module Examples.Type where
open import Agda.Builtin.Equality using (_≡_; refl)
@ -26,5 +24,5 @@ ex6 : typeToString((nil ⇒ nil) ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> nil
ex6 = refl
ex7 : typeToString((nil ⇒ nil) ∪ ((nil ⇒ (nil ⇒ nil)) ∪ nil)) ≡ "((nil) -> nil | (nil) -> (nil) -> nil)?"
ex7 = {!!}
ex7 = refl

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

@ -15,12 +15,13 @@ typeToString top = "top"
typeToString number = "number"
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) ++ " | " ++ (typeToStringᵁ T)
typeToStringᵁ T = typeToString T
typeToStringᴵ (S ∩ T) = (typeToStringᴵ S) ++ " & " ++ (typeToStringᴵ T)
typeToStringᴵ T = typeToString T