quox/tests/Tests/DimEq.idr

178 lines
5.5 KiB
Idris
Raw Normal View History

2023-03-25 15:55:28 -04:00
module Tests.DimEq
import Quox.Syntax.DimEq
import PrettyExtra
2023-05-01 21:06:25 -04:00
import AstExtra
2023-03-25 15:55:28 -04:00
import TAP
import Data.Maybe
import Data.Nat
import Data.So
-- [✓ todo] "well formed" dimeqs
-- [todo] operations maintain well-formedness
-- [todo] if 'Wf eqs' then 'equal eqs' is an equivalence
-- [todo] 'set' never breaks existing equalities
private
2023-05-14 13:58:46 -04:00
prettyDimEq_ : {opts : _} -> {default Arg prec : PPrec} ->
BContext d -> DimEq d -> Eff Pretty (Doc opts)
prettyDimEq_ [<] (C _) = pure "·"
prettyDimEq_ ds eqs = prettyDimEq ds eqs
2023-03-25 15:55:28 -04:00
private
2023-05-14 13:58:46 -04:00
testPrettyD : BContext d -> DimEq d -> (str : String) ->
2023-03-25 15:55:28 -04:00
{default str label : String} -> Test
testPrettyD ds eqs str {label} =
2023-05-14 13:58:46 -04:00
testPretty (prettyDimEq ds) eqs str str {label}
2023-03-25 15:55:28 -04:00
private
2023-05-14 13:58:46 -04:00
testWf : BContext d -> DimEq d -> Test
2023-03-25 15:55:28 -04:00
testWf ds eqs =
test (prettySquash (prettyDimEq_ ds) Unicode eqs ++ " ⊢ ✓") $
2023-03-25 15:55:28 -04:00
unless (wf eqs) $ Left ()
private
2023-05-14 13:58:46 -04:00
testNwf : BContext d -> DimEq d -> Test
2023-03-25 15:55:28 -04:00
testNwf ds eqs =
test (prettySquash (prettyDimEq_ ds) Unicode eqs ++ " ⊢ ✗") $
2023-03-25 15:55:28 -04:00
when (wf eqs) $ Left ()
private
2023-05-14 13:58:46 -04:00
testEqLabel : String -> (ds : BContext d) -> (exp, got : DimEq d) -> String
testEqLabel op ds exp got =
renderSquash $ runPrettyDef $ do
pure $ sep [!(prettyDimEq_ ds exp), text op, !(prettyDimEq_ ds got)]
2023-03-25 15:55:28 -04:00
private
2023-05-14 13:58:46 -04:00
testNeq : (ds : BContext d) -> (exp, got : DimEq d) ->
2023-03-25 15:55:28 -04:00
{default (testEqLabel "" ds exp got) label : String} -> Test
testNeq {label} ds exp got =
test label $ unless (exp /= got) $ Left ()
private
2023-05-14 13:58:46 -04:00
testEq : (ds : BContext d) -> (exp, got : DimEq d) ->
2023-03-25 15:55:28 -04:00
{default (testEqLabel "=" ds exp got) label : String} -> Test
testEq {label} ds exp got =
test label $ unless (exp == got) $
2023-05-14 13:58:46 -04:00
Left [("exp", prettySquash (prettyDimEq_ ds) Unicode exp),
("got", prettySquash (prettyDimEq_ ds) Unicode got)]
2023-03-25 15:55:28 -04:00
private
2023-05-14 13:58:46 -04:00
testSetLabel : String -> BContext d -> DimEq d ->
2023-03-25 15:55:28 -04:00
DimEq d -> List (Dim d, Dim d) -> String
2023-05-14 13:58:46 -04:00
testSetLabel op ds exp start sets = renderSquash $ runPrettyDef $ do
pure $ sep
[parens $ sep $ intersperse "/" $
!(prettyDimEq_ {prec = Outer} ds start) :: !(traverse prettySet sets),
text op, !(prettyDimEq_ ds exp)]
2023-03-25 15:55:28 -04:00
where
2023-05-14 13:58:46 -04:00
prettySet : {opts : _} -> (Dim d, Dim d) -> Eff Pretty (Doc opts)
prettySet (p, q) = pure $
hsep [!(prettyDim ds p), "", !(prettyDim ds q)]
2023-03-25 15:55:28 -04:00
private
2023-05-14 13:58:46 -04:00
testSet : (ds : BContext d) -> (exp, start : DimEq d) ->
2023-03-25 15:55:28 -04:00
(sets : List (Dim d, Dim d)) ->
(0 _ : (So (wf start), So (wf exp))) =>
Test
testSet ds exp start sets =
testEq {label = testSetLabel "=" ds exp start sets} ds exp $
foldl (\eqs, (p, q) => set p q eqs) start sets
private
2023-05-14 13:58:46 -04:00
ii, iijj, iijjkk, iijjkkll : BContext ?
2023-03-25 15:55:28 -04:00
ii = [< "𝑖"]
iijj = [< "𝑖", "𝑗"]
iijjkk = [< "𝑖", "𝑗", "𝑘"]
iijjkkll = [< "𝑖", "𝑗", "𝑘", "𝑙"]
export
tests : Test
tests = "dimension constraints" :- [
"printing" :- [
testPrettyD [<] ZeroIsOne "0 = 1",
testPrettyD iijj ZeroIsOne "𝑖, 𝑗, 0 = 1",
testPrettyD [<] new "" {label = "[empty output from empty context]"},
testPrettyD ii new "𝑖",
testPrettyD iijj (fromGround [< Zero, One])
"𝑖, 𝑗, 𝑖 = 0, 𝑗 = 1",
2023-05-01 21:06:25 -04:00
testPrettyD iijj (C [< Just (^K Zero), Nothing])
2023-03-25 15:55:28 -04:00
"𝑖, 𝑗, 𝑖 = 0",
2023-05-01 21:06:25 -04:00
testPrettyD iijjkk (C [< Nothing, Just (^BV 0), Just (^BV 1)])
2023-03-25 15:55:28 -04:00
"𝑖, 𝑗, 𝑘, 𝑗 = 𝑖, 𝑘 = 𝑖"
],
"equality" :- [
testEq [<] ZeroIsOne ZeroIsOne,
testEq [<] new new,
testEq iijj new new,
testNeq [<] new ZeroIsOne,
testNeq iijj new ZeroIsOne,
testSet iijj
2023-05-01 21:06:25 -04:00
(C [< Nothing, Just (^BV 0)])
new [(^BV 1, ^BV 0)],
2023-03-25 15:55:28 -04:00
testSet iijj
2023-05-01 21:06:25 -04:00
(C [< Nothing, Just (^BV 0)])
new [(^BV 0, ^BV 1)],
2023-03-25 15:55:28 -04:00
testNeq iijj
new
2023-05-01 21:06:25 -04:00
(C [< Nothing, Just (^BV 0)]),
2023-03-25 15:55:28 -04:00
testSet [<]
ZeroIsOne
2023-05-01 21:06:25 -04:00
new [(^K Zero, ^K One)],
2023-03-25 15:55:28 -04:00
testSet iijjkk
2023-05-01 21:06:25 -04:00
(C [< Nothing, Just (^BV 0), Just (^BV 1)])
new [(^BV 0, ^BV 1), (^BV 1, ^BV 2)],
2023-03-25 15:55:28 -04:00
testSet iijjkk
2023-05-01 21:06:25 -04:00
(C [< Nothing, Just (^BV 0), Just (^BV 1)])
new [(^BV 0, ^BV 1), (^BV 0, ^BV 2)],
2023-03-25 15:55:28 -04:00
testSet iijjkk
2023-05-01 21:06:25 -04:00
(C [< Nothing, Nothing, Just (^BV 0)])
new [(^BV 0, ^BV 1), (^BV 0, ^BV 1)],
2023-03-25 15:55:28 -04:00
testSet iijj
2023-05-01 21:06:25 -04:00
(C [< Just (^K Zero), Just (^K Zero)])
new [(^BV 1, ^K Zero), (^BV 0, ^BV 1)],
2023-03-25 15:55:28 -04:00
testSet iijjkk
2023-05-01 21:06:25 -04:00
(C [< Just (^K Zero), Just (^K Zero), Just (^K Zero)])
new [(^BV 2, ^K Zero), (^BV 1, ^BV 2), (^BV 0, ^BV 1)],
2023-03-25 15:55:28 -04:00
testSet iijjkk
2023-05-01 21:06:25 -04:00
(C [< Just (^K Zero), Just (^K Zero), Just (^K Zero)])
new [(^BV 2, ^K Zero), (^BV 0, ^BV 1), (^BV 1, ^BV 2)],
2023-03-25 15:55:28 -04:00
testSet iijjkk
2023-05-01 21:06:25 -04:00
(C [< Just (^K Zero), Just (^K Zero), Just (^K Zero)])
new [(^BV 0, ^BV 2), (^BV 1, ^K Zero), (^BV 2, ^BV 1)],
2023-03-25 15:55:28 -04:00
testSet iijjkk
2023-05-01 21:06:25 -04:00
(C [< Nothing, Just (^BV 0), Just (^BV 1)])
new [(^BV 0, ^BV 2), (^BV 2, ^BV 1)],
2023-03-25 15:55:28 -04:00
testSet iijjkkll
2023-05-01 21:06:25 -04:00
(C [< Nothing, Just (^BV 0), Just (^BV 1), Just (^BV 2)])
new [(^BV 2, ^BV 1), (^BV 3, ^BV 0), (^BV 2, ^BV 3)],
2023-03-25 15:55:28 -04:00
testSet iijjkk
2023-05-01 21:06:25 -04:00
(C [< Just (^K One), Just (^K One), Just (^K One)])
(C [< Just (^K One), Nothing, Just (^BV 0)])
[(^BV 1, ^BV 2)],
2023-03-25 15:55:28 -04:00
testSet iijj
ZeroIsOne
2023-05-01 21:06:25 -04:00
(C [< Just (^K One), Just (^K Zero)])
[(^BV 1, ^BV 0)],
2023-03-25 15:55:28 -04:00
testSet iijj
ZeroIsOne
2023-05-01 21:06:25 -04:00
(C [< Nothing, Just (^BV 0)])
[(^BV 1, ^K Zero), (^BV 0, ^K One)]
2023-03-25 15:55:28 -04:00
],
"wf" :- [
testWf [<] ZeroIsOne,
testWf ii ZeroIsOne,
testWf [<] new,
testWf iijjkk new,
2023-05-01 21:06:25 -04:00
testWf iijjkk (C [< Nothing, Just (^BV 0), Just (^BV 1)]),
testNwf iijjkk (C [< Nothing, Just (^BV 0), Just (^BV 0)]),
testWf iijj (C [< Just (^K Zero), Just (^K Zero)]),
testNwf iijj (C [< Just (^K Zero), Just (^BV 0)])
2023-03-25 15:55:28 -04:00
]
]