From f5fa63a6df90d3088d71bde0201295f1fed65dcc Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 16 Mar 2023 18:19:17 +0100 Subject: [PATCH] some pretty printing tests --- lib/Quox/Syntax/Qty.idr | 2 +- lib/Quox/Syntax/Term/Pretty.idr | 9 +- tests/Tests.idr | 3 +- tests/Tests/PrettyTerm.idr | 150 ++++++++++++++++++++++++++++++++ tests/quox-tests.ipkg | 4 +- 5 files changed, 163 insertions(+), 5 deletions(-) create mode 100644 tests/Tests/PrettyTerm.idr diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr index a4fb890..d4cbfa9 100644 --- a/lib/Quox/Syntax/Qty.idr +++ b/lib/Quox/Syntax/Qty.idr @@ -16,7 +16,7 @@ commas (x::xs) = (x <+> hl Delim ",") :: commas xs private %inline blobD : Pretty.HasEnv m => m (Doc HL) -blobD = hlF Delim $ ifUnicode "ยท" "@" +blobD = hlF Delim $ ifUnicode "ยท" "%" export %inline prettyQtyBinds : Pretty.HasEnv m => PrettyHL q => PrettyHL a => diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index 6cfd920..a752e80 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -85,7 +85,7 @@ export prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m => Maybe (Doc HL) -> f -> List a -> m (Doc HL) prettyApps pfx fun args = do - fun <- withPrec Arg $ prettyM fun + fun <- withPrec App $ prettyM fun args <- traverse (withPrec Arg . prettyArg) args parensIfM App $ hang 2 $ sep $ fun :: args where @@ -120,6 +120,11 @@ export prettyTag : TagVal -> Doc HL prettyTag t = hl Tag $ "'" <+> fromString t +-- [fixme] put delimiters around tags that aren't simple names +export +prettyTagBare : TagVal -> Doc HL +prettyTagBare t = hl Tag $ fromString t + parameters (showSubsts : Bool) mutual @@ -139,7 +144,7 @@ parameters (showSubsts : Bool) let GotPairs {init, last, _} = getPairs' [< s] t in prettyTuple $ toList $ init :< last prettyM (Enum tags) = - pure $ delims "{" "}" . aseparate comma $ map prettyTag $ + pure $ delims "{" "}" . aseparate comma $ map prettyTagBare $ Prelude.toList tags prettyM (Tag t) = pure $ prettyTag t diff --git a/tests/Tests.idr b/tests/Tests.idr index 300314a..20f7d23 100644 --- a/tests/Tests.idr +++ b/tests/Tests.idr @@ -4,6 +4,7 @@ import TAP import Tests.Reduce import Tests.Equal import Tests.Typechecker +import Tests.PrettyTerm import Tests.Lexer import Tests.Parser import Tests.FromPTerm @@ -15,11 +16,11 @@ allTests = [ Reduce.tests, Equal.tests, Typechecker.tests, + PrettyTerm.tests, Lexer.tests, Parser.tests, FromPTerm.tests, todo "DimEq", - todo "Pretty term & dim", todo "Pretty dctx/tctx/tyctx/eqctx" ] diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr new file mode 100644 index 0000000..12d1b28 --- /dev/null +++ b/tests/Tests/PrettyTerm.idr @@ -0,0 +1,150 @@ +module Tests.PrettyTerm + +import TAP +import Quox.Syntax +import Quox.Syntax.Qty.Three +import Quox.Pretty + + +squash : String -> String +squash = pack . squash' . unpack where + squash' : List Char -> List Char + squash' [] = [] + squash' (c :: cs) = + if isSpace c then + ' ' :: squash' (dropWhile isSpace cs) + else + c :: squash' cs + +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 + 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 + + testPrettyE : Elim Three d n -> String -> String -> Test + testPrettyE e uni asc = testPrettyT (E e) uni asc + + testPrettyE1 : Elim Three d n -> String -> Test + testPrettyE1 e str = testPrettyT1 (E e) str + +enum : List TagVal -> Term q d n +enum = Enum . SortedSet.fromList + +export +tests : Test +tests = "pretty printing terms" :- [ + "free vars" :- [ + testPrettyE1 [<] [<] (F "x") "x", + testPrettyE1 [<] [<] (F $ MakeName [< "A", "B", "C"] "x") "A.B.C.x" + ], + + "bound vars" :- [ + testPrettyE1 [< "๐‘–", "๐‘—"] [< "x", "y"] (BV 0) "y", + testPrettyE1 [< "๐‘–", "๐‘—"] [< "x", "y"] (BV 1) "x", + testPrettyE1 [< "๐‘–", "๐‘—"] [< "x", "y"] (F "eq" :% BV 1) "eq @๐‘–", + testPrettyE1 [< "๐‘–", "๐‘—"] [< "x", "y"] (F "eq" :% BV 1 :% BV 0) "eq @๐‘– @๐‘—" + ], + + "applications" :- [ + testPrettyE1 [<] [<] (F "f" :@ FT "x") "f x", + testPrettyE1 [<] [<] (F "f" :@@ [FT "x", FT "y"]) "f x y", + testPrettyE1 [<] [<] (F "f" :% K Zero) "f @0", + testPrettyE1 [<] [<] (F "f" :@ FT "x" :% K Zero) "f x @0", + testPrettyE1 [<] [<] (F "g" :% K One :@ FT "y") "g @1 y" + ], + + "lambda" :- [ + testPrettyT [<] [<] ([< "x"] :\\ BVT 0) "ฮป x โ‡’ x" "fun x => x", + testPrettyT [<] [<] (Lam $ SN $ FT "a") "ฮป _ โ‡’ a" "fun _ => a", + testPrettyT [<] [< "y"] ([< "x"] :\\ BVT 1) "ฮป x โ‡’ y" "fun x => y", + testPrettyT [<] [<] + ([< "x", "y", "f"] :\\ E (BV 0 :@@ [BVT 2, BVT 1])) + "ฮป x y f โ‡’ f x y" + "fun x y f => f x y", + testPrettyT [<] [<] (DLam $ SN $ FT "a") "ฮด _ โ‡’ a" "dfun _ => a", + testPrettyT [<] [<] ([< "i"] :\\% FT "x") "ฮด i โ‡’ x" "dfun i => x", + testPrettyT [<] [<] + ([< "x"] :\\ [< "i"] :\\% E (BV 0 :% BV 0)) + "ฮป x โ‡’ ฮด i โ‡’ x @i" + "fun x => dfun i => x @i" + ], + + "type universes" :- [ + testPrettyT [<] [<] (TYPE 0) "โ˜…โ‚€" "Type0", + testPrettyT [<] [<] (TYPE 100) "โ˜…โ‚โ‚€โ‚€" "Type100" + ], + + "function types" :- [ + skipWith "todo: non-dependent notation" $ + testPrettyT [<] [<] (Arr One (FT "A") (FT "B")) "A โŠธ B" "A -o B", + testPrettyT [<] [<] + (Pi_ One "x" (FT "A") (E $ F "B" :@ BVT 0)) + "(1 ยท x : A) โ†’ B x" + "(1 % x : A) -> B x", + testPrettyT [<] [<] + (Pi_ Zero "A" (TYPE 0) $ Arr Any (BVT 0) (BVT 0)) + "(0 ยท A : โ˜…โ‚€) โ†’ (ฯ‰ ยท _ : A) โ†’ A" + "(0 % A : Type0) -> (# % _ : A) -> A", + todo #"print (and parse) the below as "(A โ†  A) โ†  A""#, + testPrettyT [<] [<] + (Arr Any (Arr Any (FT "A") (FT "A")) (FT "A")) + "(ฯ‰ ยท _ : (ฯ‰ ยท _ : A) โ†’ A) โ†’ A" + "(# % _ : (# % _ : A) -> A) -> A", + todo "non-dependent, left and right nested" + ], + + "pair types" :- [ + skipWith "todo: non-dependent notation" $ + testPrettyT [<] [<] (FT "A" `And` FT "B") "A ร— B" "A ** B", + testPrettyT [<] [<] + (Sig_ "x" (FT "A") (E $ F "B" :@ BVT 0)) + "(x : A) ร— B x" + "(x : A) ** B x", + testPrettyT [<] [<] + (Sig_ "x" (FT "A") $ + Sig_ "y" (E $ F "B" :@ BVT 0) $ + E $ F "C" :@@ [BVT 1, BVT 0]) + "(x : A) ร— (y : B x) ร— C x y" + "(x : A) ** (y : B x) ** C x y", + todo "non-dependent, left and right nested" + ], + + "pairs" :- [ + testPrettyT1 [<] [<] (Pair (FT "A") (FT "B")) "(A, B)", + testPrettyT1 [<] [<] (Pair (FT "A") (Pair (FT "B") (FT "C"))) "(A, B, C)", + testPrettyT1 [<] [<] (Pair (Pair (FT "A") (FT "B")) (FT "C")) "((A, B), C)", + testPrettyT [<] [<] + (Pair ([< "x"] :\\ BVT 0) (Arr One (FT "Bโ‚") (FT "Bโ‚‚"))) + "(ฮป x โ‡’ x, (1 ยท _ : Bโ‚) โ†’ Bโ‚‚)" + "(fun x => x, (1 % _ : Bโ‚) -> Bโ‚‚)" + ], + + "enum types" :- [ + 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"}"# + ], + + "tags" :- [ + 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""# + ], + + todo "equality types", + todo "case", + todo "annotations" +] diff --git a/tests/quox-tests.ipkg b/tests/quox-tests.ipkg index 5d91630..5590c19 100644 --- a/tests/quox-tests.ipkg +++ b/tests/quox-tests.ipkg @@ -10,5 +10,7 @@ modules = Tests.Reduce, Tests.Equal, Tests.Typechecker, + Tests.PrettyTerm, Tests.Lexer, - Tests.Parser + Tests.Parser, + Tests.FromPTerm