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

Improved typeToString

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-02-09 18:31:55 -06:00
parent 74ff8c6efc
commit daa38aa29d
4 changed files with 56 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
prototyping/Examples.agda
View file

@ -4,4 +4,4 @@ module Examples where
import Examples.Syntax import Examples.Syntax
import Examples.OpSem import Examples.OpSem
import Examples.Run import Examples.Run
import Examples.Type

21
prototyping/Examples/Type.agda Normal file
View file

@ -0,0 +1,21 @@
module Examples.Type where
open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.String using (_++_)
open import Luau.Type using (nil; _∪_; _∩_; _⇒_)
open import Luau.Type.ToString using (typeToString)
ex1 : typeToString(nil) ≡ "nil"
ex1 = refl
ex2 : typeToString(nil ⇒ nil) ≡ "(nil) -> nil"
ex2 = refl
ex3 : typeToString(nil ⇒ (nil ⇒ nil)) ≡ "(nil) -> (nil) -> nil"
ex3 = refl
ex4 : typeToString(nil ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> (nil) -> nil)?"
ex4 = refl
ex5 : typeToString(nil ⇒ ((nil ⇒ nil) ∪ nil)) ≡ "(nil) -> ((nil) -> nil)?"
ex5 = refl

16
prototyping/Luau/Type.agda
View file

@ -1,5 +1,7 @@
module Luau.Type where module Luau.Type where
open import FFI.Data.Maybe using (Maybe; just; nothing)
data Type : Set where data Type : Set where
nil : Type nil : Type
_⇒_ : Type → Type → Type _⇒_ : Type → Type → Type
@ -23,3 +25,17 @@ tgt none = none
tgt any = any tgt any = any
tgt (S ∪ T) = (tgt S) ∪ (tgt T) tgt (S ∪ T) = (tgt S) ∪ (tgt T)
tgt (S ∩ T) = (tgt S) ∩ (tgt T) tgt (S ∩ T) = (tgt S) ∩ (tgt T)
optional : Type → Type
optional nil = nil
optional (T ∪ nil) = (T ∪ nil)
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 T = T

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

@ -1,13 +1,28 @@
module Luau.Type.ToString where module Luau.Type.ToString where
open import FFI.Data.String using (String; _++_) open import FFI.Data.String using (String; _++_)
open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_) open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_; normalizeOptional)
{-# TERMINATING #-}
typeToString : Type → String typeToString : Type → String
typeToStringᵁ : Type → String
typeToStringᴵ : Type → String
typeToString nil = "nil" typeToString nil = "nil"
typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T) typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
typeToString none = "none" typeToString none = "none"
typeToString any = "any" typeToString any = "any"
typeToString (S ∪ T) = (typeToString S) ++ " | " ++ (typeToString T) typeToString (S ∪ T) with normalizeOptional(S ∪ T)
typeToString (S ∩ T) = (typeToString S) ++ " & " ++ (typeToString T) typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
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