THEORY

   1 GENERAL
   2
   3  C >= D                 C is descendant of D, partial order
   4  C \haspatch D          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 \bottom meaning \notexists_{P} C \elem P.
  19
  20  For every Px, E(C,Px+)
  21    Implicitly for C \elem Pc+, E(C,Pc+) = { C }
  22    and this is not annotated explicitly.
  23    Also implicitly for P(C) = \bottom, \forall_{Px} E(C,Px+) = { }
  24    and this is also not annotated explicitly.
  25
  26 SIMPLE COMMIT
  27
  28  make C >1 { A }
  29  from A
  30
  31  with contents
  32   D \isin C <=> D \isin A v D = C
  33
  34  results
  35   P(C) = P(A)
  36   A \haspatch P <=> C \haspatch P
  37   For A \notelem Px+: E(C,Px+) = E(A,Px+)
  38       A \elem Px+: E(C,Px+) = { C } -- not annotated
  39
  40 ANTICOMMIT
  41
  42  make C >1 { L }
  43  from L, R+, R-
  44
  45  with contents
  46   D \isin C <=> D \notelement Pr+ ^ D \isin L
  47
  48  where
  49   P(R+) = Pr+, P(R-) = Pr-
  50   E(L,Pr+) = { R+ }    -- nontrivial, may need R+' = merge of E(L,Pr+)
  51   B(R+) = R-
  52   L \haspatch Pr
  53
  54  results
  55   P(C) = P(L) = Pl-
  56   If C \elem P+, B(C) = B(L); otherwise B(C) n/a
  57   For P = Pr:  C \nothaspatch Pr
  58                E(C,Pr+) = E(L,Pr+) = { R+ }
  59       P != Pr: C \haspatch P <=> L \haspatch P
  60                E(C,P+) = E(L,P+)
  61
  62 MERGE
  63
  64  make C >1 { L, R }
  65  from L, R, M
  66
  67  with contents
  68   D \isin C <=> [ (D \isin    L ^ D \isin    R) v D =  C : T            ]
  69                 [  D \notisin L ^ D \notisin R  ^ D != C : F            ]
  70                 [  otherwise                             : D \notisin M ]
  71
  72  where
  73   M < L, M < R
  74   If L \elem P+:
  75       R \elem P+ ^ B(R) = B(L)            -- only merge tips with same base
  76     v R \elem P- ^ R >= B(L) ^ M = B(L)   -- base when merging into tip
  77   If L \elem P-:
  78       R \nothaspatch P
  79   If L \haspatch P <=/=> R \haspatch P:
  80       \forall Ce \elem E(R,P+): Ce <= L   -- may need to merge E(R,P+) into L
  81
  82  results
  83   P(C) = P(L)
  84   B(C) =
  85     For C \notelem P+:             n/a
  86         C \elem P+, R \elem P+:    B(L) = B(R)
  87         C \elem P+, R \notelem P+: R >= B(L)
  88
  89   C \haspatch P =
  90     For L \nothaspatch P, R \nothaspatch P: F
  91         L \haspatch P,    R \haspatch P:    T
  92         otherwise:                          M \nothaspatch P
  93   E(C,P+) = maximal elements of E(L,P+) \union E(R,P+)
  94           = { Cl | \notexist Cr \elem E(R,P+): Cr >= Cl } \union
  95             { Cr | \notexist Cl \elem E(L,P+): Cl >= Cr }
  96
  97  -- to reintroduce a dep, set P(C)=P(L)=Pl-, P(R)=Pr+, M=B(R)
  98     where L \notelem Pr obv.
  99
 100
 101 CREATE BASE
 102
 103  make B >1 { L }
 104  from L, P
 105
 106  where
 107   P(L) = Pl+ v P(L) = \bottom
 108   P(L) != P(B)
 109   E(B,P+) = { }
 110
 111  with contents
 112   D \isin B <=> D \isin L v D = B
 113
 114  results
 115   P(B) = Pb-
 116   B(C) n/a
 117   E(B,Px+) = E(L,Px+)
 118   B \haspatch P <=> L \haspatch P
 119
 120
 121 CREATE TIP
 122
 123  make C >1 { B}
 124  from B
 125
 126  where
 127   B \elem Pb-
 128   E(B,P+) = { }
 129
 130  with contents
 131   D \isin C <=> D \isin B v D = C
 132
 133  results
 134   P(C) = Pb+
 135   B(C) = B
 136   C \haspatch P =
 137     For P != Pb: B \haspatch P
 138         P = Pb:  T