X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke.git;a=blobdiff_plain;f=THEORY;h=f40a1fc5848ad786e51b61a17b15e89e27c7e807;hp=e908c6838a22c471af7d2a794739ea3a4de7254f;hb=a2bee3f9f4ecc497a19a96a2f6b1264a1f9809e7;hpb=8acb4aba1948cee65c773e1d0c199e190dc4837f

diff --git a/THEORY b/THEORY
index e908c68..f40a1fc 100644
--- a/THEORY
+++ b/THEORY
@@ -1,56 +1,138 @@
-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 ] D
-	C ] D => C > D
-
-patches
-	patch P is two subset of commits, Ptip and Pbase
-	each subset has a single ur-ancestor C0_Ptip resp C0_Pbase
-	these subsets mutually exclusive
-	P(C) is either Ptip, Pbase, or nil (recorded in commit)
-
-commits fall into three categories wrt P
- how(P,C) = included
-	P included in C
-		\forall D \elem Ptip,  C ] D <=> C > D
- how(P,C) = absent
-	P absent from C
-		\forall D \elem Ptip, !(C ] D)
- how(P,C) = removed
-	P removed from C
-		\exists E s.t.
-			\forall D \elem Ptip,
-				something
-
-the ends E(C,Px) of Px = Pbase or Ptip are
-	every maximal Ce < C in Px ie
-	every Ce for which
-		C > Ce   ^   !\exists C s.t. C > Ce
-
-cleanness of patch
-	if P(C) = Ptip
-	   B \elem E(C,Pbase)
-	then
-	   C ] Cx  ^  B !] Cx  =>  P
-
-normal commits
- make C from D
- result
-	C < { D }
-	P(C) = P(D)
-	Cx [ C  <=>  Cx = D  v  Cx [ D
-	how(P,C) = how(P,D)
-
-anticommit
- make C from D, P, A-, 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)
+ Patch inclusion
+   C \haspatch P    <=> [ \forall D \elem P+: D \isin C <=> D <= C ]
+   C \nothaspatch P <=> [ \forall D \elem P+: D \notisin C ]
+
+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
+  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
-	A+ < A- < D
-	E(D,Ptip) = { A- }
-	E(D,Pbase) = { A+ }
- result
-	C < { D }
-	P(C) = P(D)
-	
+  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
+  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