[darcs-devel] [patch1911] WIP: use Prim patches in rebase toedit

[Ben Franksen]

Ben Franksen <ben.franksen at online.de> added the comment:

>>> It could even be (FL prim :> prim) but then it's not very obvious that
>>> some are fixups and some aren't.
>>
>> (except perhaps if you create a new data type for the whole thing)
>>
>>> Given that it's in a Named, that then expands to
>>>
>>>  FL ((FL (PrimFixup prim) :> prim)
>>>
>>> which is a bit annoying but we need some way to express the fact that at
>>> any point there can be zero or more PrimFixups.
>>
>> See above.
> 
> I don't think a new datatype can help with the fundamental structure of
> the type - some way or another, the end result inside a Named will need
> to be isomorphic to FL (FL prim :> prim).

Of course. I thought you were worried about readability. I think in the
end we need something like

  RebaseContainer prim ~ Suspended prim ~ FL RebaseChange prim
  RebaseChange prim ~ FL RebaseName :> Named (Unwound prim)

where Unwound is a single prim with fixups before and possibly after.
RebaseFixup and RebaseItem no longer make sense.

BTW, forceCommute for prims is not hard to define. I just made up the
following definition (it typechecks but is untested):

data Unwound prim wX wY where
  Unwound :: FL prim wX wA
          -> prim wA wB
          -> FL prim wB wY
          -> Unwound prim wX wY

forceCommute
  :: (Commute prim, Invert prim)
  => (prim :> prim) wX wY -> (Unwound prim :> Unwound prim) wX wY
forceCommute (p :> q) =
  case commute (p :> q) of
    Just (q' :> p') -> Unwound NilFL q' NilFL :> Unwound NilFL p' NilFL
    Nothing ->
      Unwound (singleFL p) q (singleFL (invert q))
      :>
      Unwound (singleFL (invert p)) p (singleFL q)
  where
    singleFL x = x :>: NilFL

__________________________________
Darcs bug tracker <bugs at darcs.net>
<http://bugs.darcs.net/patch1911>
__________________________________