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

Remove extra space in anonymous functions

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-02-11 18:46:43 -06:00
parent 34030da631
commit a4595ac24f
2 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
prototyping/Examples/Syntax.agda
View file

@ -6,7 +6,7 @@ open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←
open import Luau.Syntax.ToString using (exprToString; blockToString) open import Luau.Syntax.ToString using (exprToString; blockToString)
ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡ ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡
"function (x)\n" ++ "function(x)\n" ++
" return f(x)\n" ++ " return f(x)\n" ++
"end" "end"
ex1 = refl ex1 = refl

12
prototyping/Luau/Syntax/ToString.agda
View file

@ -11,8 +11,10 @@ varDecToString (var x) = varToString x
varDecToString (var x ∈ T) = varToString x ++ " : " ++ typeToString T varDecToString (var x ∈ T) = varToString x ++ " : " ++ typeToString T
funDecToString : ∀ {a} → FunDec a → String funDecToString : ∀ {a} → FunDec a → String
funDecToString (f ⟨ x ⟩∈ T) = varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T funDecToString ("" ⟨ x ⟩∈ T) = "function(" ++ varDecToString x ++ "): " ++ typeToString T
funDecToString (f ⟨ x ⟩) = varToString f ++ "(" ++ varDecToString x ++ ")" funDecToString ("" ⟨ x ⟩) = "function(" ++ varDecToString x ++ ")"
funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T
funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")"
exprToString′ : ∀ {a} → String → Expr a → String exprToString′ : ∀ {a} → String → Expr a → String
statToString′ : ∀ {a} → String → Stat a → String statToString′ : ∀ {a} → String → Stat a → String
@ -27,16 +29,16 @@ exprToString′ lb (var x) =
exprToString′ lb (M $ N) = exprToString′ lb (M $ N) =
(exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")" (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
exprToString′ lb (function F is B end) = exprToString′ lb (function F is B end) =
"function " ++ funDecToString F ++ lb ++ funDecToString F ++ lb ++
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
"end" "end"
exprToString′ lb (block b is B end) = exprToString′ lb (block b is B end) =
"(function " ++ b ++ "()" ++ lb ++ "(" ++ b ++ "()" ++ lb ++
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
"end)()" "end)()"
statToString′ lb (function F is B end) = statToString′ lb (function F is B end) =
"local function " ++ funDecToString F ++ lb ++ "local " ++ funDecToString F ++ lb ++
" " ++ (blockToString′ (lb ++ " ") B) ++ lb ++ " " ++ (blockToString′ (lb ++ " ") B) ++ lb ++
"end" "end"
statToString′ lb (local x ← M) = statToString′ lb (local x ← M) =