Fix important bug in shrinking

[edsko]

Consider shrinking a set of commands such as

Commands [
    Command cmd1           (S.fromList [Var 0])
  , Command cmd2           (S.fromList [Var 1])
  , Command (cmd3 (Var 1)) (S.fromList [])
  ]

Shrinking is basically a call to QuickCheck's shrinkList followed by a validation step, the core of which is implemented in validCommands. validCommands executes each command, checking preconditions, and checking which variables are in scope, and (effectively) renaming variables. For example, given the shrink candidate

Commands [
    -- first command deleted
    Command cmd2           (S.fromList [Var 1])
  , Command (cmd3 (Var 1)) (S.fromList [])
  ]

validCommands will reexecute cmd2, find all is well, construct

    Command cmd2           (S.fromList [Var 0]) -- variable 0 instead of 1

However, when it then gets to cmd3, it finds that Var 1 is not in scope, and regard the shrink candidate as invalid. This however is not correct: cmd3 refers to the result of cmd2, which is still in the shrunk program! Conversely, if the original program was

Commands [
    Command cmd1           (S.fromList [Var 0])
  , Command cmd2           (S.fromList [Var 1])
  , Command (cmd3 (Var 0)) (S.fromList [])
  ]

instead, with cmd3 referring to the output of the first command, then the same shrink candidate

Commands [
    -- first command deleted
    Command cmd2           (S.fromList [Var 1])
  , Command (cmd3 (Var 0)) (S.fromList [])
  ]

should now be rejected (after all, cmd3 refers to the output of cmd1, which has been deleted), but instead may not be, and result in the "validated" program

Commands [
    -- first command deleted
    Command cmd2           (S.fromList [Var 0])
  , Command (cmd3 (Var 0)) (S.fromList [])
  ]

where cmd3 suddenly referse to cmd2 instead.

Instead of merely keeping track of the scope, therefore, we need to keep track of this remapping of variables, constructing the validated program

Commands [
    -- first command deleted
    Command cmd2           (S.fromList [Var 0])
  , Command (cmd3 (Var 0)) (S.fromList [])
  ]

for the first example, and rejecting the second example.

This is implemented in this patch. The essence of the patch is the logic in go in validCommands. It has a few small knock-on effect:

• In order to be able to translate commands we need cmd to be Rank2.Traversable rather than merely Rank2.Foldable
• It is important that we precise about the order of the variables returned by commands; therefore using a set rather than a list in Command is not correct.
• The internal state of validCommands now uses a Map rather than a Set, which requires a few trivial updates to other functions that are defined in terms of validCommands.

[edsko]

This is technically a breaking change, as it changes some exposed functions and types, but I think the impact should be minimal, as those types/functions are in what's effectively q-s-m's internal API.

[edsko]

Re-pushed with signoff.

[edsko]

Thanks for the quick response! By the way, heads up: I am planning to write a blog post soon about the effective use of q-s-m. If you like I can send you a link to a draft if you want to proofread it before publishing. Don't at all feel obliged though :)

[stevana]

@edsko: I'd be happy to!

[edsko]

Awesome :) Would you be able to fire off a quick email to edsko@well-typed.com so that I have your email address and I can email you a link to the draft before publishing?

[stevana]

Done!