quote tags in printing if they're not identifiers

lib/Quox/Syntax/Term/Pretty.idr

@@ -115,10 +115,20 @@ prettyCase pi elim r ret arms = do
   arms <- prettyArms arms
   pure $ asep [caseD <++> elim, returnD <++> ret, ofD <++> arms]
 
+export
+escapeString : String -> String
+escapeString = concatMap esc1 . unpack where
+  esc1 : Char -> String
+  esc1 '"'  = #"\""#
+  esc1 '\\' = #"\\"#
+  esc1 '\n' = #"\n"#
+  esc1 c    = singleton c
+
 export
 quoteTag : TagVal -> Doc HL
 quoteTag tag =
-  if isName tag then fromString tag else hcat ["\"", fromString tag, "\""]
+  if isName tag then fromString tag else
+  hcat ["\"", fromString $ escapeString tag, "\""]
 
 export
 prettyTag : TagVal -> Doc HL

tests/Tests/PrettyTerm.idr

@@ -7,7 +7,7 @@ import Quox.Pretty
 
 
 squash : String -> String
-squash = pack . squash' . unpack where
+squash = pack . squash' . unpack . trim where
   squash' : List Char -> List Char
   squash' [] = []
   squash' (c :: cs) =
@@ -20,21 +20,26 @@ renderSquash : Doc HL -> String
 renderSquash = squash . ($ "") . renderShow . layoutCompact
 
 parameters (ds : NContext d) (ns : NContext n)
-  testPrettyT : Term Three d n -> String -> String -> Test
-  testPrettyT t uni asc = test {e = Info} uni $ do
-    let uni' = renderSquash $ prettyTerm True  ds ns t
+  testPrettyT : Term Three d n -> (uni, asc : String) ->
+                {default uni label : String} -> Test
+  testPrettyT t uni asc {label} = test {e = Info} label $ do
+    let uni  = squash uni; asc = squash asc
+        uni' = renderSquash $ prettyTerm True  ds ns t
         asc' = renderSquash $ prettyTerm False ds ns t
     unless (squash uni == uni') $ Left [("exp", uni), ("got", uni')]
     unless (squash asc == asc') $ Left [("exp", asc), ("got", asc')]
 
-  testPrettyT1 : Term Three d n -> String -> Test
-  testPrettyT1 t str = testPrettyT t str str
+  testPrettyT1 : Term Three d n -> (str : String) ->
+                 {default str label : String} -> Test
+  testPrettyT1 t str {label} = testPrettyT t str str {label}
 
-  testPrettyE : Elim Three d n -> String -> String -> Test
-  testPrettyE e uni asc = testPrettyT (E e) uni asc
+  testPrettyE : Elim Three d n -> (uni, asc : String) ->
+                {default uni label : String} -> Test
+  testPrettyE e uni asc {label} = testPrettyT (E e) uni asc {label}
 
-  testPrettyE1 : Elim Three d n -> String -> Test
-  testPrettyE1 e str = testPrettyT1 (E e) str
+  testPrettyE1 : Elim Three d n -> (str : String) ->
+                 {default str label : String} -> Test
+  testPrettyE1 e str {label} = testPrettyT1 (E e) str {label}
 
 enum : List TagVal -> Term q d n
 enum = Enum . SortedSet.fromList
@@ -132,14 +137,17 @@ tests = "pretty printing terms" :- [
     testPrettyT1 [<] [<] (enum []) "{}",
     testPrettyT1 [<] [<] (enum ["a"]) "{a}",
     testPrettyT1 [<] [<] (enum ["aa", "bb", "cc"]) "{aa, bb, cc}",
-    testPrettyT1 [<] [<] (enum ["a b c"]) #"{"a b c"}"#
+    testPrettyT1 [<] [<] (enum ["a b c"]) #"{"a b c"}"#,
+    testPrettyT1 [<] [<] (enum ["\"", ",", "\\"]) #" {"\"", ",", \} "#
+      {label = #"{"\"", ",", \}  # ｢\｣ is an identifier"#}
   ],
 
   "tags" :- [
     testPrettyT1 [<] [<] (Tag "a") "'a",
     testPrettyT1 [<] [<] (Tag "hello") "'hello",
     testPrettyT1 [<] [<] (Tag "qualified.tag") "'qualified.tag",
-    testPrettyT1 [<] [<] (Tag "non-identifier tag") #"'"non-identifier tag""#
+    testPrettyT1 [<] [<] (Tag "non-identifier tag") #"'"non-identifier tag""#,
+    testPrettyT1 [<] [<] (Tag #"""#) #" '"\"" "#
   ],
 
   todo "equality types",