On Fri, Aug 15, 2008 at 10:05 AM, Jason Dagit <[EMAIL PROTECTED]> wrote:
>
>
> On Fri, Aug 15, 2008 at 7:38 AM, David Roundy <[EMAIL PROTECTED]> wrote:
>
>> 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 <[EMAIL PROTECTED]>
>> > * major refactor of SelectChanges to work with type witnesses
>> >
>> > Tue Aug 12 22:04:25 PDT 2008 Jason Dagit <[EMAIL PROTECTED]>
>> > * refine type witnesses in SelectChanges
>> >
>> > Thu Aug 14 22:39:58 PDT 2008 Jason Dagit <[EMAIL PROTECTED]>
>> > * 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?
>
>
> Sure, but I've invested all my waking time into this refactor for several
> days.
>
>
>>
>>
>> > 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 <[EMAIL PROTECTED]>**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.
>
>
> In that case I'll try to stop refactoring the existing code and fix the
> bug(s) that prevent it from having that type signature.
>
I realize it's probably not at all clear what bugs I'm talking about. So
let me try to explain myself visually.
By inspecting wspfr, we see that the last parameter sequence it takes is
never shortened, only added to. If we represent all the involved patch
sequences as going from left to right, the input sequences look like this:
[() ... p_1 ] :: C(() r) and [ pend ] :: C(r u), where u is just the state
after the pending and p_1 is the patch most recently applied to the
repository.
After some number of steps in wspfr we have this:
[() ... p_n ] :: C(() a) and [p_{n-1} ... (p_1 :: C(? r), pend :: C(r u) ]
:: C(a u)
Now, before we return to the caller, we do a commuteFL:
commuteFL ( p_n :> [ p_{n-1} ... p_1, pend] ) :: C(? u). This results in
this output:
[p'_{n-1} ... p'_1, (pend' :: C(r_1 u_1)] :> (p'_n :: C(u_1 u)
The important bit here is that we don't have pend anymore, we have pend'.
Now we return these results to the caller.
Then, with_selected_patches_from_repository does this commute:
commute( pend' :: C(r_1 u_1) :> p'_n :: C(u_1 u) ) -> ( p''_n :: C(r_1 u_2)
:> pend'' :: C(u_2 u))
It turns out that since we had *just* commuted p'_n with pend', we know that
pend'' == pend, and p''_n == p_n. We've just done step one of commuting
p''_n past [ p'_{n-1} .. p'_1, pend']. Which means we get p'_n back to
where it was before we returned from wspfr. Then we apply job to ( p_n ::
C(? a), [ p'_{n-1} ... p'_1 ] :: C(?? r_1) ).
As you can see, unless we also commute p_n past the [p'_{n-1} .. p'_1], then
there is no way we can be sure that r_1 = r.
Jason
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
