chiark / gitweb /
new THEORY, proved
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Wed, 22 Feb 2012 10:47:45 +0000 (10:47 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Wed, 22 Feb 2012 10:47:45 +0000 (10:47 +0000)
THEORY

diff --git a/THEORY b/THEORY
index d0fdab5..5dd24c3 100644 (file)
--- a/THEORY
+++ b/THEORY
-relations
-       ancestry: of commits, a partial order
-               C > D           C is a descendant of D
-       inclusion: commit includes change made in another
-               a partial order, consistent with ancestry but more partial
-               C has D <=> D isin C
-       C has D => C > D
-
-define convenience function
-       cont(C) := { Cx | Cx isin C }
-
-patches
-       patch P is two sets Px of commits, Ptip and Pbase
-       each subset has a single ur-ancestor C0_Ptip resp C0_Pbase
-       all these subsets Ptip,Qbase,Rtip,Sbase mutually exclusive
-       P(C) is either Ptip, Pbase, or nil (recorded in commit)
-
-commits fall into three categories wrt P
- inpatch(P,C) = included
-       P included in C
-               \forall D \elem Ptip,  C has D <=> C > D
- inpatch(P,C) = absent
-       P absent from C
-               \forall D \elem Ptip, !(C has D)
- inpatch(P,C) = removed
-       P removed from C
-               cont(C) \intersection Ptip = { }
-               but maybe \exists Cx \elem Ptip s.t. Cx < C
-
-the ends E(C,Px) of Px = Pbase or Ptip are
-       every maximal Ce < C in Px
-       ie every Ce for which
-               C > Ce   and   !\exists C s.t. C > Ce
-
-existence of corresponding base B for every tip commit C
-       \forall C s.t. P(C) = Ptip
-               \exists B s.t. E(C,Pbase) = { B }
- resulting function B(C)
-
-contents of tip commits
-       \forall C s.t. P(c) = Ptip
-               cont(C) = cont(B(C)) \union { Cp s.t. P(Cp) = Ptip and Cp < C }
-
-non-circularity
-       \forall B s.t. P(c) = Pbase
-               cont(B) \notintersect Ptip
-
-normal commits
- make C from D
- result
-       C < { D }
-       P(C) = P(D)
-       Cx isin C  <=>  Cx = D  v  Cx isin D
-       inpatch(P,C) = inpatch(P,D)
-
-anticommit for removing a patch P from D to make C
- make C from D, A-
+GENERAL
+
+ C >= D                        C is descendant of D, partial order
+ C \haspatch D         C contains changes from D, partial order
+ Patch P has two sets P+, P-
+ Ancestors A(C,P) = { Ca \elem C | Ca \elem P }
+ Ends E(C,P) = maximal elements of A(C,P)
+
+COMMIT ANNOTATIONS
+
+ Commit C is annotated with:
+
+ P(C)
+   Either P s.t. C \elem P
+   or \bottom meaning \notexists_{P} C \elem P.
+
+ For every Px, E(C,Px+)
+   Implicitly for C \elem Pc+, E(C,Pc+) = { C } 
+   and this is not annotated explicitly.
+   Also implicitly for P(C) = \bottom, \forall_{Px} E(C,Px+) = { }
+   and this is also not annotated explicitly.
+
+SIMPLE COMMIT
+
+ make C >1 { A } 
+ from A
+
+ with contents
+  D \isin C <=> D \isin A v D = C
+
+ results
+  P(C) = P(A)
+  A \haspatch P <=> C \haspatch P
+  For A \notelem Px+: E(C,Px+) = E(A,Px+)
+      A \elem Px+: E(C,Px+) = { C } -- not annotated
+
+ANTICOMMIT
+
+ make C >1 { L }
+ from L, R+, R- 
+
+ with contents
+  D \isin C <=> D \notelement Pr+ ^ D \isin L
+
+ where
+  P(R+) = Pr+, P(R-) = Pr-
+  E(L,Pr+) = { R+ }    -- nontrivial, may need R+' = merge of E(L,Pr+)
+  B(R+) = R-
+  L \haspatch Pr
+
+ results
+  P(C) = P(L) = Pl-
+  If C \elem P+, B(C) = B(L); otherwise B(C) n/a
+  For P = Pr:  C \nothaspatch Pr
+               E(C,Pr+) = E(L,Pr+) = { R+ }
+      P != Pr: C \haspatch P <=> L \haspatch P
+               E(C,P+) = E(L,P+)
+
+MERGE
+
+ make C >1 { L, R }
+ from L, R, M
+
+ with contents
+  D \isin C <=> [ (D \isin    L ^ D \isin    R) v D =  C : T            ]
+                [  D \notisin L ^ D \notisin R  ^ D != C : F            ]
+                [  otherwise                             : D \notisin M ]
+
  where
-       P(C) = Qbase
-       P(A-) = Ptip
-       inpatch(P,C) = included
-       E(D,Ptip) = { A- }
- then let
-       A+ = B(A-)
- hence
-       A+ < A- < D
-       E(D,Pbase) = { A+ }
- result
-       C >1 { D }
-       P(C) = P(D)
-       inpatch(P,C) = removed
-
-single patch dependency application
- make C from D, A+
+  M < L, M < R
+  If L \elem P+:
+      R \elem P+ ^ B(R) = B(L)            -- only merge tips with same base
+    v R \elem P- ^ R >= B(L) ^ M = B(L)   -- base when merging into tip
+  If L \elem P-:
+      R \nothaspatch P
+  If L \haspatch P <=/=> R \haspatch P:
+      \forall Ce \elem E(R,P+): Ce <= L   -- may need to merge E(R,P+) into L
+
+ results
+  P(C) = P(L)
+  B(C) = 
+    For C \notelem P+:             n/a
+        C \elem P+, R \elem P+:    B(L) = B(R)
+        C \elem P+, R \notelem P+: R >= B(L)
+
+  C \haspatch P =
+    For L \nothaspatch P, R \nothaspatch P: F
+        L \haspatch P,    R \haspatch P:    T
+        otherwise:                          M \nothaspatch P
+  E(C,P+) = maximal elements of E(L,P+) \union E(R,P+)
+          = { Cl | \notexist Cr \elem E(R,P+): Cr >= Cl } \union
+            { Cr | \notexist Cl \elem E(L,P+): Cl >= Cr }
+
+ -- to reintroduce a dep, set P(C)=P(L)=Pl-, P(R)=Pr+, M=B(R)
+    where L \notelem Pr obv.
+
+
+CREATE BASE
+
+ make B >1 { L }
+ from L, P
+
  where
-       P(C) = Qbase
-       P(A+) = Ptip
-       inpatch(P,C) != included
- then let
-       A- = B(A+)
- hence
-       A- < A+
- result
-       C >1 { D, A+ } => C > D, C > A+ > A-
-       P(C) = P(D)
-       inpatch(P,C) = included
-
-simple merge
- make C from L, R, M
+  P(L) = Pl+ v P(L) = \bottom
+  P(L) != P(B)
+  E(B,P+) = { }
+
+ with contents
+  D \isin B <=> D \isin L v D = B
+
+ results
+  P(B) = Pb-
+  B(C) n/a
+  E(B,Px+) = E(L,Px+)
+  B \haspatch P <=> L \haspatch P
+
+
+CREATE TIP
+
+ make C >1 { B}
+ from B
+
  where
-       M < L < C
-       M < R < C
- result
-       C >1 { L, R }
-       P(C) = P(L)
-       if Cx isin L = Cx isin R,
-               Cx isin C = Cx isin L
-       otherwise
-               Cx isin C = ! Cx isin M
-       
-  cases of inpatch(P,L) and ,R
-               
-         or    Cx isin 
+  B \elem Pb-
+  E(B,P+) = { }
+
+ with contents
+  D \isin C <=> D \isin B v D = C
+
+ results
+  P(C) = Pb+
+  B(C) = B
+  C \haspatch P =
+    For P != Pb: B \haspatch P
+        P = Pb:  T