quox/tests/Tests/PrettyTerm.idr

190 lines
6.5 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Tests.PrettyTerm
import TAP
import Quox.Syntax
import Quox.Syntax.Qty.Three
import Quox.Pretty
squash : String -> String
squash = pack . squash' . unpack . trim 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 -> (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 -> (str : String) ->
{default str label : String} -> Test
testPrettyT1 t str {label} = testPrettyT t str str {label}
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 -> (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
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 "(AA)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" :- [
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}",
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 #"""#) #" '"\"" "#
],
todo "equality types",
"case" :- [
testPrettyE [<] [<]
(CasePair One (F "a") (SN $ TYPE 1) (SN $ TYPE 0))
"case1 a return _ ⇒ ★₁ of { (_, _) ⇒ ★₀ }"
"case1 a return _ => Type1 of { (_, _) => Type0 }",
testPrettyT [<] [<]
([< "u"] :\\
E (CaseEnum One (F "u")
(SY [< "x"] $ Eq0 (enum ["tt"]) (BVT 0) (Tag "tt"))
(fromList [("tt", [< Unused] :\\% Tag "tt")])))
"λ u ⇒ case1 u return x ⇒ x ≡ 'tt : {tt} of { 'tt ⇒ δ _'tt }"
"""
fun u =>
case1 u return x => x == 'tt : {tt} of { 'tt => dfun _ => 'tt }
"""
],
"annotations" :- [
testPrettyE [<] [<] (FT "a" :# FT "A") "a ∷ A" "a :: A",
testPrettyE [<] [<]
(FT "a" :# E (FT "A" :# FT "𝐀"))
"a ∷ A ∷ 𝐀"
"a :: A :: 𝐀",
testPrettyE [<] [<]
(E (FT "α" :# FT "a") :# FT "A")
"(α ∷ a) ∷ A"
"(α :: a) :: A",
testPrettyE [<] [<]
(([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A"))
"(λ x ⇒ x) ∷ 1.A → A"
"(fun x => x) :: 1.A -> A",
testPrettyE [<] [<]
(Arr One (FT "A") (FT "A") :# TYPE 7)
"(1.A → A) ∷ ★₇"
"(1.A -> A) :: Type7"
]
]