[darcs-users] darcs patch: major refactor of SelectChanges to work ... (and 2 more)

[David Roundy]

On Thu, Aug 14, 2008 at 10:43:33PM -0700, Jason Dagit wrote:
> David,
> 
> I don't think the last patch will compile with modules that use select
> changes but I do think this version might be what you were expecting.  If
> so I'll amend-record the last patch so that it compiles everywhere.
> 
> Let me know what you think.
> 
> Thanks,
> Jason
> 
> Tue Aug 12 20:16:25 PDT 2008  Jason Dagit <dagit at codersbase.com>
>   * major refactor of SelectChanges to work with type witnesses
> 
> Tue Aug 12 22:04:25 PDT 2008  Jason Dagit <dagit at codersbase.com>
>   * refine type witnesses in SelectChanges
> 
> Thu Aug 14 22:39:58 PDT 2008  Jason Dagit <dagit at codersbase.com>
>   * Potentially correct SelectChanges

See below.  This is getting closer, but isn't quite right.  Good news
is that I'm convinced that once it's right, you won't need
unsafeCoerceP.  :)

I believe there were also other similar select functions that I
suggested you rewrite.  Those are still in the queue?

> hunk ./src/Darcs/SelectChanges.lhs 214
> -wspfr :: RepoPatch p => String -> (PatchInfoAnd p -> Bool)
> -      -> RL (PatchInfoAnd p) -> [PatchInfoAnd p]
> -      -> IO (Maybe (PatchInfoAnd p, [PatchInfoAnd p]))
> +wspfr :: RepoPatch p => String -> (FORALL(a b) (PatchInfoAnd p) C(a b) -> Bool)
> +      -> RL (PatchInfoAnd p) C(x y) -> FL (PatchInfoAnd p) C(y z)
> +      -> IO (Maybe (FlippedSeal (FL (PatchInfoAnd p) :> (PatchInfoAnd p)) C(z)))

> [Potentially correct SelectChanges
> Jason Dagit <dagit at codersbase.com>**20080815053958] hunk ./src/Darcs/SelectChanges.lhs 48
> -import Darcs.Patch.Ordered ( FL(..), RL(..), (:>)(..),
> -                             (+>+), lengthFL, concatRL, mapFL_FL,
> +import Darcs.Patch.Ordered ( FL(..), RL(..), (:>)(..), EqCheck(..),
> +                             (+>+), lengthFL, concatRL, mapFL_FL, (=/\=),
> hunk ./src/Darcs/SelectChanges.lhs 193
> -with_selected_patch_from_repo :: RepoPatch p => String -> Repository p C(r u t) -> [DarcsFlag] -> Bool
> -                              -> (FORALL(a b) ((FL (PatchInfoAnd p) :> (PatchInfoAnd p)) C(a b)) -> IO ()) -> IO ()
> +with_selected_patch_from_repo :: forall p C(r u t). RepoPatch p => String -> Repository p C(r u t) -> [DarcsFlag] -> Bool
> +                              -> (FORALL(a b) ((FL (PatchInfoAnd p)) C(a r), ((PatchInfoAnd p) C(r b))) -> IO ()) -> IO ()

No, this isn't quite right, and that's what's leading to your
unsafeCoerceP below.  This should be:

with_selected_patch_from_repo
         :: forall p C(r u t). RepoPatch p => String
         -> Repository p C(r u t) -> [DarcsFlag] -> Bool
         -> (FORALL(a) ((FL (PatchInfoAnd p) :> PatchInfoAnd p) C(a r))) -> IO ()) -> IO ()

which is to say that since we're selecting a patch from the repo, the
final state had better be the recorded state.  With this type
signature, the sloppyEquals shouldn't be required--which is to say,
you should be able to use =/\= directly... you're completely right
that an equality check is needed here.

> hunk ./src/Darcs/SelectChanges.lhs 200
> +    let pend_ = n2pia $ anonymous $ fromPrims pend
> hunk ./src/Darcs/SelectChanges.lhs 202
> -                              (concatRL p_s) ((n2pia $ anonymous $ fromPrims pend) :>: NilFL)
> +                              (concatRL p_s) (pend_ :>: NilFL)
> hunk ./src/Darcs/SelectChanges.lhs 206
> -           pend':<:skipped ->
> -            case commute (pend' :> selected) of
> -            Just (selected' :> _) -> job (reverseRL skipped :> selected')
> -            Nothing -> impossible
> +           pend' :<: skipped ->
> +            -- Due to the way wspfr always leaves the pending as the last patch
> +            -- in the s_and_pend portion of it's return value, this test should
> +            -- always be true and it tells the type system that pend_ and pend'
> +            -- are equal and hence have the same contexts.
> +            case pend_ `sloppyEquals` pend' of
> +            IsEq ->
> +              case commute (pend' :> selected) of
> +                    Just (selected' :> _) -> job (reverseRL skipped, selected')
> +                    Nothing -> impossible
> +            _ -> impossible
> hunk ./src/Darcs/SelectChanges.lhs 221
> +  where
> +  sloppyEquals :: (PatchInfoAnd p) C(x y) -> (PatchInfoAnd p) C(q v) -> EqCheck C(x q)
> +  sloppyEquals p1 p2 = p1 =/\= (unsafeCoerceP p2)

David