It is a relatively new and complicated part of the Hakaru simplification process, and almost all test cases contain piecewise and all piecewise will spend some (most) time as Partitions. It stands to reason that Partition could use some unit tests. In #85, we decided this would be a good way of ensuring certain nice properties which we would like on the Haskell side, as implementing Partition on the Haskell side is likely more trouble than it's worth.
[ ] A corpus of Partitions representative of the typical Partitions that are seen while simplifying Hakaru programs is needed. Collecting such a corpus from the test cases should be straightforward. We should collect both those Partitions which are unsimplified and simplified. This should probably include some sums of Partitions and products of Partitions with scalars.
[ ] The properties which we want to hold need to be identified. Each property should apply to every Partition in the corpus; potentially, a property may hold on a given unsimplified Partition only after it has been simplified. The properties already known:
PWToPartition @ PartitionToPW is the identity
PartitionToPW @ PWToPartition is the identity (this is somewhat less necessary)
Partition:-Simpl is idempotent
x->Partition:-Simpl(x,do_solve) is idempotent
(x->PWToPartition(x,do_solve)) @ PartitionToPW is idempotent
PartitionToPW @ (x->PWToPartition(x,do_solve)) is idempotent
It's unclear if we want these properties to hold up to list semantics (i.e. propositional equality) or up to SamePartition (which gives set semantics to Partitions).
It is a relatively new and complicated part of the Hakaru simplification process, and almost all test cases contain
piecewiseand allpiecewisewill spend some (most) time as Partitions. It stands to reason that Partition could use some unit tests. In #85, we decided this would be a good way of ensuring certain nice properties which we would like on the Haskell side, as implementing Partition on the Haskell side is likely more trouble than it's worth.PWToPartition @ PartitionToPWis the identityPartitionToPW @ PWToPartitionis the identity (this is somewhat less necessary)Partition:-Simplis idempotentx->Partition:-Simpl(x,do_solve)is idempotent(x->PWToPartition(x,do_solve)) @ PartitionToPWis idempotentPartitionToPW @ (x->PWToPartition(x,do_solve))is idempotentIt's unclear if we want these properties to hold up to list semantics (i.e. propositional equality) or up to
SamePartition(which gives set semantics to Partitions).