rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

equality tests

Browse source
This commit is contained in:
rhiannon morris 2022-05-09 18:31:43 +02:00
parent a26eba7d7f
commit 89f9793143
1 changed files with 48 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

91
tests/Tests/Equal.idr
View file

@ -52,19 +52,19 @@ export
tests : Test tests : Test
tests = "equality & subtyping" :- [ tests = "equality & subtyping" :- [
"universes" :- [ "universes" :- [
testEq "★₀ ≡ ★₀" $ testEq "★₀ ≡ ★₀" $
equalT (TYPE 0) (TYPE 0), equalT (TYPE 0) (TYPE 0),
testNeq "★₀ ≢ ★₁" $ testNeq "★₀ ≢ ★₁" $
equalT (TYPE 0) (TYPE 1), equalT (TYPE 0) (TYPE 1),
testNeq "★₁ ≢ ★₀" $ testNeq "★₁ ≢ ★₀" $
equalT (TYPE 1) (TYPE 0), equalT (TYPE 1) (TYPE 0),
testEq "★₀ <: ★₀" $ testEq "★₀ <: ★₀" $
subT (TYPE 0) (TYPE 0), subT (TYPE 0) (TYPE 0),
testEq "★₀ <: ★₁" $ testEq "★₀ <: ★₁" $
subT (TYPE 0) (TYPE 1), subT (TYPE 0) (TYPE 1),
testNeq "★₁ ≮: ★₀" $ testNeq "★₁ ≮: ★₀" $
subT (TYPE 1) (TYPE 0) subT (TYPE 1) (TYPE 0)
], ],
"pi" :- [ "pi" :- [
-- ⊸ for →₁, ⇾ for →₀ -- ⊸ for →₁, ⇾ for →₀
@ -129,39 +129,44 @@ tests = "equality & subtyping" :- [
todo "term d-closure", todo "term d-closure",
"free var" :- [ "free var" :- [
testEq "A ≡ A" $ testEq "A ≡ A" $
equalE (F "A") (F "A"), equalE (F "A") (F "A"),
testNeq "A ≢ B" $ testNeq "A ≢ B" $
equalE (F "A") (F "B"), equalE (F "A") (F "B"),
testEq "A <: A" $ testEq "A <: A" $
subE (F "A") (F "A"), subE (F "A") (F "A"),
testNeq "A ≮: B" $ testNeq "A ≮: B" $
subE (F "A") (F "B") subE (F "A") (F "B")
], ],
todo "bound var", "bound var" :- [
testEq "#0 ≡ #0" $
equalE (BV 0) (BV 0) {n = 1},
testNeq "#0 ≢ #1" $
equalE (BV 0) (BV 1) {n = 2}
],
"application" :- [ "application" :- [
testEq "f [a] ≡ f [a]" $ testEq "f [a] ≡ f [a]" $
equalE (F "f" :@ FT "a") (F "f" :@ FT "a"), equalE (F "f" :@ FT "a") (F "f" :@ FT "a"),
testEq "f [a] <: f [a]" $ testEq "f [a] <: f [a]" $
subE (F "f" :@ FT "a") (F "f" :@ FT "a"), subE (F "f" :@ FT "a") (F "f" :@ FT "a"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A) (β)" $ testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A) (β)" $
equalE equalE
((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
:@ FT "a") :@ FT "a")
(E (FT "a" :# FT "A") :# FT "A"), (E (FT "a" :# FT "A") :# FT "A"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a (βυ)" $ testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a (βυ)" $
equalE equalE
((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
:@ FT "a") :@ FT "a")
(F "a"), (F "a"),
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $ testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
subE subE
((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
:@ FT "a") :@ FT "a")
(F "a") (F "a")
], ],
todo "annotation", todo "annotation",