THEORY

   1 relations
   2         ancestry: of commits, a partial order
   3                 C > D           C is a descendant of D
   4         inclusion: commit includes change made in another
   5                 a partial order, consistent with ancestry but more partial
   6                 C has D <=> D isin C
   7         C has D => C > D
   8
   9 define convenience function
  10         cont(C) := { Cx | Cx isin C }
  11
  12 patches
  13         patch P is two sets Px of commits, Ptip and Pbase
  14         each subset has a single ur-ancestor C0_Ptip resp C0_Pbase
  15         all these subsets Ptip,Qbase,Rtip,Sbase mutually exclusive
  16         P(C) is either Ptip, Pbase, or nil (recorded in commit)
  17
  18 commits fall into three categories wrt P
  19  inpatch(P,C) = included
  20         P included in C
  21                 \forall D \elem Ptip,  C has D <=> C > D
  22  inpatch(P,C) = absent
  23         P absent from C
  24                 \forall D \elem Ptip, !(C has D)
  25  inpatch(P,C) = removed
  26         P removed from C
  27                 cont(C) \intersection Ptip = { }
  28                 but maybe \exists Cx \elem Ptip s.t. Cx < C
  29
  30 the ends E(C,Px) of Px = Pbase or Ptip are
  31         every maximal Ce < C in Px
  32         ie every Ce for which
  33                 C > Ce   and   !\exists C s.t. C > Ce
  34
  35 existence of corresponding base B for every tip commit C
  36         \forall C s.t. P(C) = Ptip
  37                 \exists B s.t. E(C,Pbase) = { B }
  38  resulting function B(C)
  39
  40 contents of tip commits
  41         \forall C s.t. P(c) = Ptip
  42                 cont(C) = cont(B(C)) \union { Cp s.t. P(Cp) = Ptip and Cp < C }
  43
  44 non-circularity
  45         \forall B s.t. P(c) = Pbase
  46                 cont(B) \notintersect Ptip
  47
  48 normal commits
  49  make C from D
  50  result
  51         C < { D }
  52         P(C) = P(D)
  53         Cx isin C  <=>  Cx = D  v  Cx isin D
  54         inpatch(P,C) = inpatch(P,D)
  55
  56 anticommit for removing a patch P from D to make C
  57  make C from D, A-
  58  where
  59         P(C) = Qbase
  60         P(A-) = Ptip
  61         inpatch(P,C) = included
  62         E(D,Ptip) = { A- }
  63  then let
  64         A+ = B(A-)
  65  hence
  66         A+ < A- < D
  67         E(D,Pbase) = { A+ }
  68  result
  69         C >1 { D }
  70         P(C) = P(D)
  71         inpatch(P,C) = removed
  72
  73 single patch dependency application
  74  make C from D, A+
  75  where
  76         P(C) = Qbase
  77         P(A+) = Ptip
  78         inpatch(P,C) != included
  79  then let
  80         A- = B(A+)
  81  hence
  82         A- < A+
  83  result
  84         C >1 { D, A+ } => C > D, C > A+ > A-
  85         P(C) = P(D)
  86         inpatch(P,C) = included
  87