1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Errors
module type S = sig
module Branch :
sig
type t
val make : string -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val to_string : t -> string
val master : t
end
type id
(* Branches have [branch_info] attached to them. *)
type ('kind) branch_info = {
kind : [> `Master] as 'kind;
root : id;
pos : id;
}
type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
val empty : id -> ('kind,'diff,'info) t
val current_branch : ('k,'e,'i) t -> Branch.t
val branches : ('k,'e,'i) t -> Branch.t list
val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info
val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t
val branch :
('kind,'e,'i) t -> ?root:id -> ?pos:id ->
Branch.t -> 'kind -> ('kind,'e,'i) t
val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
val merge :
('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
Branch.t -> ('k,'diff,'i) t
val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t
val rewrite_merge :
('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
Branch.t -> ('k,'diff,'i) t
val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
val get_info : ('k,'e,'info) t -> id -> 'info option
module NodeSet : Set.S with type elt = id
val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
val reachable : ('k,'e,'info) t -> id -> NodeSet.t
module Dag : Dag.S with type node = id
val dag : ('kind,'diff,'info) t -> ('diff,'info,id*id) Dag.t
val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t
val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option
val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t
end
module Make(OT : Map.OrderedType) = struct
module Dag = Dag.Make(OT)
type id = OT.t
module NodeSet = Dag.NodeSet
module Branch =
struct
type t = string
let make =
let bid = ref 0 in
fun s -> incr bid; string_of_int !bid ^ "_" ^ s
let equal = CString.equal
let compare = CString.compare
let to_string s = s
let master = "master"
end
module BranchMap = Map.Make(Branch)
type 'kind branch_info = {
kind : [> `Master] as 'kind;
root : id;
pos : id;
}
type ('kind,'edge,'info) t = {
cur_branch : Branch.t;
heads : 'kind branch_info BranchMap.t;
dag : ('edge,'info,id*id) Dag.t;
}
let empty root = {
cur_branch = Branch.master;
heads = BranchMap.singleton Branch.master { root = root; pos = root; kind = `Master };
dag = Dag.empty;
}
let add_node vcs id edges =
assert (not (CList.is_empty edges));
{ vcs with dag =
List.fold_left (fun g (t,tgt) -> Dag.add_edge g id t tgt) vcs.dag edges }
let get_branch vcs head =
try BranchMap.find head vcs.heads
with Not_found -> anomaly (str"head " ++ str head ++ str" not found")
let reset_branch vcs head id =
let map name h =
if Branch.equal name head then { h with pos = id } else h
in
{ vcs with heads = BranchMap.mapi map vcs.heads; }
let current_branch vcs = vcs.cur_branch
let branch
vcs ?(root=(get_branch vcs vcs.cur_branch).pos) ?(pos=root) name kind
=
{ vcs with
heads = BranchMap.add name { kind; root; pos } vcs.heads;
cur_branch = name }
let delete_branch vcs name =
if Branch.equal Branch.master name then vcs else
let filter n _ = not (Branch.equal n name) in
{ vcs with heads = BranchMap.filter filter vcs.heads }
let merge vcs id ~ours:tr1 ~theirs:tr2 ?(into = vcs.cur_branch) name =
assert (not (Branch.equal name into));
let br_id = (get_branch vcs name).pos in
let cur_id = (get_branch vcs into).pos in
let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
let vcs = reset_branch vcs into id in
vcs
let del_edge id vcs tgt = { vcs with dag = Dag.del_edge vcs.dag id tgt }
let rewrite_merge vcs id ~ours:tr1 ~theirs:tr2 ~at:cur_id name =
let br_id = (get_branch vcs name).pos in
let old_edges = List.map fst (Dag.from_node vcs.dag id) in
let vcs = List.fold_left (del_edge id) vcs old_edges in
let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
vcs
let commit vcs id tr =
let vcs = add_node vcs id [tr, (get_branch vcs vcs.cur_branch).pos] in
let vcs = reset_branch vcs vcs.cur_branch id in
vcs
let checkout vcs name = { vcs with cur_branch = name }
let set_info vcs id info = { vcs with dag = Dag.set_info vcs.dag id info }
let get_info vcs id = Dag.get_info vcs.dag id
let create_cluster vcs l i = { vcs with dag = Dag.create_cluster vcs.dag l i }
let cluster_of vcs i = Dag.cluster_of vcs.dag i
let delete_cluster vcs c = { vcs with dag = Dag.del_cluster vcs.dag c }
let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads []
let dag vcs = vcs.dag
let rec closure s d n =
let l = try Dag.from_node d n with Not_found -> [] in
List.fold_left (fun s (n',_) ->
if Dag.NodeSet.mem n' s then s
else closure s d n')
(Dag.NodeSet.add n s) l
let reachable vcs i = closure Dag.NodeSet.empty vcs.dag i
let gc vcs =
let alive =
BranchMap.fold (fun b { pos } s -> closure s vcs.dag pos)
vcs.heads Dag.NodeSet.empty in
let dead = Dag.NodeSet.diff (Dag.all_nodes vcs.dag) alive in
{ vcs with dag = Dag.del_nodes vcs.dag dead }, dead
end
|
