102 lines
2.5 KiB
Idris
102 lines
2.5 KiB
Idris
|
module Tests.Equal
|
||
|
|
|
||
|
|
import Quox.Equal
|
||
|
|
import Quox.Pretty
|
||
|
|
import TAP
|
||
|
|
|
||
|
|
export
|
||
|
|
ToInfo Equal.Error where
|
||
|
|
toInfo (ClashT mode s t) =
|
||
|
|
[("clash", "term"),
|
||
|
|
("mode", show mode),
|
||
|
|
("left", prettyStr True s),
|
||
|
|
("right", prettyStr True t)]
|
||
|
|
toInfo (ClashU mode k l) =
|
||
|
|
[("clash", "universe"),
|
||
|
|
("mode", show mode),
|
||
|
|
("left", prettyStr True k),
|
||
|
|
("right", prettyStr True l)]
|
||
|
|
toInfo (ClashQ pi rh) =
|
||
|
|
[("clash", "quantity"),
|
||
|
|
("left", prettyStr True pi),
|
||
|
|
("right", prettyStr True rh)]
|
||
|
|
|
||
|
|
|
||
|
|
M = Error [Equal.Error]
|
||
|
|
|
||
|
|
testEq : String -> Lazy (M ()) -> Test
|
||
|
|
testEq = test
|
||
|
|
|
||
|
|
testNeq : String -> Lazy (M ()) -> Test
|
||
|
|
testNeq = testThrows
|
||
|
|
|
||
|
|
|
||
|
|
subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
|
||
|
|
subT = Quox.Equal.subT
|
||
|
|
%hide Quox.Equal.subT
|
||
|
|
|
||
|
|
equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
|
||
|
|
equalT = Quox.Equal.equalT
|
||
|
|
%hide Quox.Equal.equalT
|
||
|
|
|
||
|
|
subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
|
||
|
|
subE = Quox.Equal.subE
|
||
|
|
%hide Quox.Equal.subE
|
||
|
|
|
||
|
|
equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
|
||
|
|
equalE = Quox.Equal.equalE
|
||
|
|
%hide Quox.Equal.equalE
|
||
|
|
|
||
|
|
|
||
|
|
export
|
||
|
|
tests : Test
|
||
|
|
tests = "equality & subtyping" :- [
|
||
|
|
"universes" :- [
|
||
|
|
testEq "Type 0 == Type 0" $
|
||
|
|
equalT (TYPE (U 0)) (TYPE (U 0)),
|
||
|
|
testNeq "Type 0 =/= Type 1" $
|
||
|
|
equalT (TYPE (U 0)) (TYPE (U 1)),
|
||
|
|
testNeq "Type 1 =/= Type 0" $
|
||
|
|
equalT (TYPE (U 1)) (TYPE (U 0)),
|
||
|
|
testEq "Type 0 <: Type 0" $
|
||
|
|
subT (TYPE (U 0)) (TYPE (U 0)),
|
||
|
|
testEq "Type 0 <: Type 1" $
|
||
|
|
subT (TYPE (U 0)) (TYPE (U 1)),
|
||
|
|
testNeq "Type 1 </: Type 0" $
|
||
|
|
subT (TYPE (U 1)) (TYPE (U 0))
|
||
|
|
],
|
||
|
|
todo "pi",
|
||
|
|
todo "lambda",
|
||
|
|
todo "term closure",
|
||
|
|
todo "term d-closure",
|
||
|
|
|
||
|
|
"free var" :- [
|
||
|
|
testEq "A == A" $
|
||
|
|
equalE (F "A") (F "A"),
|
||
|
|
testNeq "A =/= B" $
|
||
|
|
equalE (F "A") (F "B"),
|
||
|
|
testEq "A <: A" $
|
||
|
|
subE (F "A") (F "A"),
|
||
|
|
testNeq "A </: B" $
|
||
|
|
subE (F "A") (F "B")
|
||
|
|
],
|
||
|
|
todo "bound var",
|
||
|
|
"application" :-
|
||
|
|
let a = F "a"; a' = E a
|
||
|
|
A = FT "A"
|
||
|
|
λxx = Lam "x" (TUsed (BVT 0))
|
||
|
|
A_A = Arr one A A
|
||
|
|
λxx' = λxx :# A_A
|
||
|
|
in [
|
||
|
|
testEq "(λx. x : A -> A) a == ((a : A) : A) (β)" $
|
||
|
|
equalE (λxx' :@ a') (E (a' :# A) :# A),
|
||
|
|
testEq "(λx. x : _) a == a (βυ)" $
|
||
|
|
equalE (λxx' :@ a') a
|
||
|
|
],
|
||
|
|
todo "annotation",
|
||
|
|
todo "elim closure",
|
||
|
|
todo "elim d-closure",
|
||
|
|
|
||
|
|
todo "clashes"
|
||
|
|
]
|