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

a few more tests

Browse source
This commit is contained in:
rhiannon morris 2022-05-27 18:00:06 +02:00
parent cd651558a2
commit da91f7d95e
1 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
tests/Tests/Reduce.idr
View file

@ -94,8 +94,11 @@ tests = "whnf" :- [
"term closure" :- [ "term closure" :- [
testWhnfT "(λy. x){a/x}" testWhnfT "(λy. x){a/x}"
(CloT (Lam "x" $ TUnused $ BVT 0) (F "a" ::: id)) (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
(Lam "x" $ TUnused $ FT "a") (Lam "y" $ TUnused $ FT "a"),
testWhnfT "(λy. y){a/x}"
(CloT (Lam "y" $ TUsed $ BVT 0) (F "a" ::: id))
(Lam "y" $ TUsed $ BVT 0)
], ],
"looking inside […]" :- [ "looking inside […]" :- [
@ -111,6 +114,10 @@ tests = "whnf" :- [
(Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0, (Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0,
testNoStepE "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $ testNoStepE "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
F "a" :@ F "a" :@
E ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a") E ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
testNoStepT "λx. [y [x]]{x/x,a/y}" {n = 1} $
Lam "x" $ TUsed $ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
testNoStepE "f ([y [x]]{x/x,a/y})" {n = 1} $
F "f" :@ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id)
] ]
] ]