On Fri, Aug 15, 2008 at 2:30 PM, David Roundy <[EMAIL PROTECTED]> wrote:
> On Tue, Aug 12, 2008 at 10:54 PM, Jason Dagit <[EMAIL PROTECTED]> > wrote: > > David, > > > > I started adding type witnesses to Unrevert and I'm not quite sure how > > to proceed. > > > > You'll probably want to apply this patch to see the error messages. > > > > In unrevert_cmd, we use get_common_and_uncommon to find the patches > > that need to be merged. Next we try to call considerMergeToWorking. > > > > I think that this code is making an assumption about the return value > > of get_common_and_uncommon. considerMergeToWorking takes two sequences, > > FL p C(u x), and FL p C(u y). When I was working on > considerMergeToWorking > > I almost made this a merge pair, :\/:, but I realized the relationship to > > repository's unrecorded state might be handy. So, I think the > > considerMergeToWoring signature is correct. > > > > One problem here is get_common_and_uncommon doesn't break the returned > > patch sets at u. > > > > What's worse is that we assume that if we take the head of both sides of > the > > returned pair from get_common_and_uncommon that those lists start from > > the same context. I briefly glanced at the guts of > get_common_and_uncommon > > again and I don't see how the guts ensure that would be the case. > Although, > > I admit that's a pretty tricky function. > > This is some remaining stupidity in get_common_and_uncommon, which > really should be fixed (but not necessarily now). It turns out, if > you look carefully, that the tail of either output of > get_common_and_uncommon is always NilRL. This is very stupid, and > dates way back (and is all my fault). get_common_and_uncommon really > ought to have type: > > get_common_and_uncommon :: RepoPatch p => (PatchSet p C(x),PatchSet p C(y)) > -> > ([PatchInfo],(RL (PatchInfoAnd p) :\/: RL > (PatchInfoAnd p)) C(x y)) > > which only differs in that it's got a simple RL rather than a nested > RL (RL ...). Ah, interesting. I hadn't picked up on that. There is still one problem though...see below. > I can see two simple workarounds for this: one would be to simply > pattern match on (h_us:<:NilRL) and leave any other case in the > "impossible" category. The other would be to simply use concatRL, > which in this case is equivalent to headRL, except in type. I think > the former possibility is slightly cleaner, as it documents the > stupidity in the interface. But if my analysis is wrong and there > really is a bug, then you won't have fixed the bug, you'll just have > made it exit with an error message. Even if I use the patten match above, we have the problem that considerMergeToWorking needs to know that both patch sequences start from the unrecorded state. So, I'm left wondering how to extract that proof from get_common_and_uncommon. I feed get_common_and_uncommon two sequences, us :: C(() r), and them :: C(() a). Actually, I'm not confident that them should be a patchset. I hava feeling it's supposed to be them :: C(a b) when I look at how it was constructed. But if that's the case then it wouldn't even be safe to call get_common_and_uncommon. It's created by reading the repository's unrevert then doing a scan_bundle on that to convert to a PatchSet, but I find it hard to believe that scan_bundle returns a patchset. It seems more likley that scan_bundle returns an RL (RL p)) C(x y), and it's up to the caller to tell scan_bundle the true meaning of those contexts. I need to think about this more and figure out what state is the unrevert in at any time. If you have time for me discussion today, I look forward to anything other info you can pass on :) Thanks! Jason
_______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
