diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr index 757f612..9420e36 100644 --- a/lib/Quox/Name.idr +++ b/lib/Quox/Name.idr @@ -128,3 +128,11 @@ baseName = idStart <+> many idCont <+> many idEnd export name : Lexer name = baseName <+> many (is '.' <+> baseName) + + +export +isName : String -> Bool +isName str = + case scan name [] (unpack str) of + Just (_, []) => True + _ => False diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index a752e80..ce4adfe 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -115,15 +115,18 @@ prettyCase pi elim r ret arms = do arms <- prettyArms arms pure $ asep [caseD <++> elim, returnD <++> ret, ofD <++> arms] --- [fixme] put delimiters around tags that aren't simple names +export +quoteTag : TagVal -> Doc HL +quoteTag tag = + if isName tag then fromString tag else hcat ["\"", fromString tag, "\""] + export prettyTag : TagVal -> Doc HL -prettyTag t = hl Tag $ "'" <+> fromString t +prettyTag t = hl Tag $ "'" <+> quoteTag t --- [fixme] put delimiters around tags that aren't simple names export prettyTagBare : TagVal -> Doc HL -prettyTagBare t = hl Tag $ fromString t +prettyTagBare t = hl Tag $ quoteTag t parameters (showSubsts : Bool) diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr index 12d1b28..9b1f883 100644 --- a/tests/Tests/PrettyTerm.idr +++ b/tests/Tests/PrettyTerm.idr @@ -132,7 +132,6 @@ tests = "pretty printing terms" :- [ testPrettyT1 [<] [<] (enum []) "{}", testPrettyT1 [<] [<] (enum ["a"]) "{a}", testPrettyT1 [<] [<] (enum ["aa", "bb", "cc"]) "{aa, bb, cc}", - skipWith "todo: quote non-identifiers" $ testPrettyT1 [<] [<] (enum ["a b c"]) #"{"a b c"}"# ], @@ -140,7 +139,6 @@ tests = "pretty printing terms" :- [ testPrettyT1 [<] [<] (Tag "a") "'a", testPrettyT1 [<] [<] (Tag "hello") "'hello", testPrettyT1 [<] [<] (Tag "qualified.tag") "'qualified.tag", - skipWith "todo: quote non-identifiers" $ testPrettyT1 [<] [<] (Tag "non-identifier tag") #"'"non-identifier tag""# ],