quox/tests/Tests/PrettyTerm.idr

170 lines
5.8 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 PrettyExtra
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} =
testPretty (toSnocList' ds) (toSnocList' ns) t uni asc {label}
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}
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"
]
]