TODO
====
A non-exhaustive list of things TO DO for Extrapolate.
WARNING: This TO DO list is outdated.
* `deriveGeneralizable` should `deriveListableIfNeeded`.
examples
--------
* `ideal-generalizations`:
Add examples of ideal generalizations as described in past paper by human
experts. The counter example is `blah` because the property fails for every
`bleh` and `blih`. I found:
- one on Duregard's licentiate Thesis: `prop_cycle` from `BNFC-meta`.
- one on Duregard's doctorate Thesis.
- one on SmallCheck's paper: `prop_insertRB` from RedBlack
there are none on:
- QuickCheck
- Testing and Tracing with Quickcheck and Hat
- SmartCheck
- Feat
- Real World Haskell
- Learn-you-a-haskell
- Growing and shrinking polygons
- QuickFuzz
* `add-th-eg`:
add the parser example from the Feat paper;
* `apply-lazysmallcheck`:
apply Lazy SmallCheck to calculator and parse and record the results.
feature
-------
* `deriveGeneralizableAtomic`: derive a generalizable value treating it as
atomic, as I did with the Map on the XMonad example. To be used on datatypes
with data invariants.
* `deriveGeneralizableFromTo`: derive a generalizable value using a bijection
passed as parameter so that a data invariant is not broken. Example:
deriveGeneralizable ''Map fromList toList.
* `background-exclusion`:
add a mechanism to exclude functions from the background.
* `report-multiple-generalizations`:
when there is more than one generalization and they don't encompass
one-another, report both.
* `detect-silly-conditionals`:
eg:
xs when 0 /= length xs
that's just:
_:_
the above is for the last property of the list example
* `renaming`:
possibly print `(Div (C 0) (Add (C x) (C (negate x))))`
which is equivalent to `(Div (C 0) (Add (C x) (C y))) when y == negate x`
instead of `(Div (C 0) (Add (C 0) (C 0)))`;
I got it to print the middle one, by just: `-- not (isAssignment wc)` and
`constant "negate" (negate -:> x) in the background`.
* `improve-record-printing`:
Improve the record printing by explictly printing records and _not_ showing
variables. For example, when testing `prop_delete`, currently we get:
StackSet (Screen (Workspace x y (Just s)) z x’) ss ws crs
but we could get instead, with the actual following indentation:
> check prop_delete
StackSet { current = Screen
{ workspace = Workspace
{ tag = x
, layout = y
, stack = Just s
}
, screen = z
, screenDetail = x'
}
, visible = ss
, hidden = ws
, floating = crs
}
which could be further summarized to:
stackset {current = scr {workspace = ws {stack = Just s}}}
performance and improvements in the algorithm (only later)
----------------------------------------------------------
* `type-after-type`:
to improve performance, instead of working with all types at once, perform
the algorithm type after type
* `single-then-multi`:
only do vassignments *after* finding a failing single variable instance.
I'll have to re-test, but the time I save may pay off.
* `new-lgg-algorithm`:
This is just a sketch:
1. test and keep all tests that pass and fail
2. pick first counter-example, note that it does not match any of the passing
tests
3. first counter-example is current generalization
4. compute lgg of current generalization with the next counter-example
5. if it does not matches any of the passing tests, update current generalization
6. go to 4
7. generalize to several variables
Variation of steps 4 and 5 with conditions:
4. compute lgg of current generaliation with the next counter-example,
find weakest condition for it to hold
5. if lgg matches 10% of failing tests, update current generalization.
The variation may have trouble when dealing with multiple variables,
maybe there should be a multi-lgg, or start with all vars different
After some tests, I see that this does not quite work as expected. c.f.
`union xs ys == union ys xs`. When incorporating a counterExample, sometimes
the generalization will temporarily match some passing tests, only to be
later weeded out by some other counter-example. There are many many more
combinations of counterexamples 2^#nce then there are candidate
generalizations of the smallest counter-example (at least in the worst case,
maybe there is a property here that I am not seeing).
won't fix
---------
* `nlp-example`:
add the NLP example from the SmartCheck paper. I don't think I'll use this
because of a few issues.
GenI has the bit-rot:
- GenI 0.24.3 refuses to build on GHC 8.0.1;
- GenI 0.24.3 builds on GHC 7.8 but test files are missing;
- The version on git is the most up-to-date contradicting the fact that it is
supposed to be a mirror from Darcs. It does not seem to be building on
Travis. It has tests, but I have not tried compiling it.
Lee Pike's paper does not list the exact property and fault for which
SmartCheck recuces its counterexample. I also looked at the TeX comments,
and the info is also not there. The mentioned stackoverflow question does
not help with that either. I could certainly ask of course if I choose to
carry on with this.
Thinking again, maybe it is a good idea to use this. It is a real library
with real bugs in the git history.
* `enlarge-default-background`:
I tried enlarging the default background by including (&&) and (||). Not
only there is no effect in the output of the build-in examples, runtime
increases for up to 33%.
I also tried enlarging the default background by including functions over
lists from the prelude, such as: (:), last, reverse, init. Runtime increases
by 10x, with no interesting effect on output (most changes are just
rewritings of the unconditional generalization.