[darcs-users] darcs patch: partial type witnesses in Unrevert

[Jason Dagit]

On Fri, Aug 15, 2008 at 2:30 PM, David Roundy <droundy at darcs.net> wrote:

> On Tue, Aug 12, 2008 at 10:54 PM, Jason Dagit <dagit at codersbase.com>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.osuosl.org/pipermail/darcs-users/attachments/20080815/35fcb21f/attachment.htm