diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index ce4adfe..9c40c63 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/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 diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr index 48d0f00..4f13a62 100644 --- a/tests/Tests/PrettyTerm.idr +++ b/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",