THEORY

   1 GENERAL
   2
   3  C >= D                 C is descendant of D, partial order
   4  D \isin C              C contains changes from D, partial order
   5  Patch P has two sets P+, P-
   6  Ancestors A(C,P) = { Ca \elem C | Ca \elem P }
   7  Ends E(C,P) = maximal elements of A(C,P)
   8  Patch inclusion
   9    C \haspatch P    <=> [ \forall D \elem P+: D \isin C <=> D <= C ]
  10    C \nothaspatch P <=> [ \forall D \elem P+: D \notisin C ]
  11
  12 COMMIT ANNOTATIONS
  13
  14  Commit C is annotated with:
  15
  16  P(C)
  17    Either P s.t. C \elem P
  18    or _|_ meaning \notexists_{P} C \elem P.
  19
  20  { Pi | C \haspatch Pi }
  21    ie the set of included patches
  22
  23  For every Px, E(C,Px+)
  24    Implicitly for C \elem Pc+, E(C,Pc+) = { C }
  25    and this is not annotated explicitly.
  26    Also implicitly for P(C) = _|_, \forall_{Px} E(C,Px+) = { }
  27    and this is also not annotated explicitly.
  28
  29  B(C)
  30    For C \elem P+:       B s.t. E(C,P-) = { B }
  31        P(C) = P- or _|_: _|_
  32
  33  Of these in principle all except P(C) can be recalculated from the
  34  commit history, but that would involve a complete history scan and in
  35  the case of \haspatch is clearly impractical.  At some point we may
  36  provide a checker/sanitiser that recalculates E(C,Px+) and B(C) from
  37  the commit history.
  38
  39 SIMPLE COMMIT
  40
  41  make C >1 { A }
  42  from A
  43
  44  with contents
  45   D \isin C <=> D \isin A v D = C
  46
  47  results
  48   P(C) = P(A)
  49   A \haspatch P <=> C \haspatch P
  50   For A \notelem Px+: E(C,Px+) = E(A,Px+)
  51       A \elem Px+: E(C,Px+) = { C } -- not annotated
  52
  53 ANTICOMMIT
  54
  55  make C >1 { L }
  56  from L, R+, R-
  57
  58  with contents
  59   D \isin C <=> D \notelement Pr+ ^ D \isin L
  60
  61  where
  62   P(R+) = Pr+, P(R-) = Pr-
  63   E(L,Pr+) = { R+ }    -- nontrivial, may need R+' = merge of E(L,Pr+)
  64   B(R+) = R-
  65   L \haspatch Pr
  66
  67  results
  68   P(C) = P(L) = Pl-
  69   If C \elem P+, B(C) = B(L); otherwise B(C) n/a
  70   For P = Pr:  C \nothaspatch Pr
  71                E(C,Pr+) = E(L,Pr+) = { R+ }
  72       P != Pr: C \haspatch P <=> L \haspatch P
  73                E(C,P+) = E(L,P+)
  74
  75 MERGE
  76
  77  make C >1 { L, R }
  78  from L, R, M
  79
  80  with contents
  81   D \isin C <=> [ (D \isin    L ^ D \isin    R) v D =  C : T            ]
  82                 [  D \notisin L ^ D \notisin R  ^ D != C : F            ]
  83                 [  otherwise                             : D \notisin M ]
  84
  85  where
  86   M < L, M < R
  87   If L \elem P+:
  88       R \elem P+ ^ B(R) = B(L)            -- only merge tips with same base
  89     v R \elem P- ^ R >= B(L) ^ M = B(L)   -- base when merging into tip
  90   If L \elem P-:
  91       R \nothaspatch P
  92   If L \haspatch P <=/=> R \haspatch P:
  93       \forall Ce \elem E(R,P+): Ce <= L   -- may need to merge E(R,P+) into L
  94
  95  results
  96   P(C) = P(L)
  97   B(C) =
  98     For C \notelem P+:             n/a
  99         C \elem P+, R \elem P+:    B(L) = B(R)
 100         C \elem P+, R \notelem P+: R >= B(L)
 101
 102   C \haspatch P =
 103     For L \nothaspatch P, R \nothaspatch P: F
 104         L \haspatch P,    R \haspatch P:    T
 105         otherwise:                          M \nothaspatch P
 106   E(C,P+) = maximal elements of E(L,P+) \union E(R,P+)
 107           = { Cl | \notexist Cr \elem E(R,P+): Cr >= Cl } \union
 108             { Cr | \notexist Cl \elem E(L,P+): Cl >= Cr }
 109
 110  -- to reintroduce a dep, set P(C)=P(L)=Pl-, P(R)=Pr+, M=B(R)
 111     where L \notelem Pr obv.
 112
 113
 114 CREATE BASE
 115
 116  make B >1 { L }
 117  from L, P
 118
 119  where
 120   P(L) = Pl+ v P(L) = _|_
 121   P(L) != P(B)
 122   E(B,P+) = { }
 123
 124  with contents
 125   D \isin B <=> D \isin L v D = B
 126
 127  results
 128   P(B) = Pb-
 129   B(C) n/a
 130   E(B,Px+) = E(L,Px+)
 131   B \haspatch P <=> L \haspatch P
 132
 133
 134 CREATE TIP
 135
 136  make C >1 { B}
 137  from B
 138
 139  where
 140   B \elem Pb-
 141   E(B,P+) = { }
 142
 143  with contents
 144   D \isin C <=> D \isin B v D = C
 145
 146  results
 147   P(C) = Pb+
 148   B(C) = B
 149   C \haspatch P =
 150     For P != Pb: B \haspatch P
 151         P = Pb:  T