chiark / gitweb /
new THEORY, define inpatch
[topbloke.git] / 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