From d75da809429d5d2d40d108608db9e5acd9aec9c9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 May 2016 11:08:37 +0200 Subject: STM: support for nested boxes of nodes to model error boundaries Dag extended to support arbitrary clusters, renamed to Property. Vcs generalized to not impose the data hold by a Property. Stm(VCS) names a property "a box" and imposes a topological invariant (no overlap). It defines 2 kind of boxes: ProofTasks (the old cluster notion) and ErrorBound (meant to confine errors to sub-proofs). In the meanwhile more equations added to Make(..) functors in order to have just one Stateid.Set module around. --- stm/dag.ml | 94 +++++++++++++++++++++---------------- stm/dag.mli | 50 +++++++++++--------- stm/stm.ml | 151 ++++++++++++++++++++++++++++++++++++++++++------------------ stm/vcs.ml | 75 +++++++++++++++--------------- stm/vcs.mli | 66 ++++++++++++++------------ 5 files changed, 260 insertions(+), 176 deletions(-) (limited to 'stm') diff --git a/stm/dag.ml b/stm/dag.ml index 0c7f9f34b..99e7c9264 100644 --- a/stm/dag.ml +++ b/stm/dag.ml @@ -8,15 +8,6 @@ module type S = sig - module Cluster : - sig - type 'd t - val equal : 'd t -> 'd t -> bool - val compare : 'd t -> 'd t -> int - val to_string : 'd t -> string - val data : 'd t -> 'd - end - type node module NodeSet : Set.S with type elt = node @@ -31,45 +22,57 @@ module type S = sig val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t val all_nodes : ('e,'i,'d) t -> NodeSet.t - val iter : ('e,'i,'d) t -> - (node -> 'd Cluster.t option -> 'i option -> - (node * 'e) list -> unit) -> unit - - val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t - val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option - val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t - val get_info : ('e,'i,'d) t -> node -> 'i option val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t + module Property : + sig + type 'd t + val equal : 'd t -> 'd t -> bool + val compare : 'd t -> 'd t -> int + val to_string : 'd t -> string + val data : 'd t -> 'd + val having_it : 'd t -> NodeSet.t + end + + val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t + val property_of : ('e,'i,'d) t -> node -> 'd Property.t list + val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t + + val iter : ('e,'i,'d) t -> + (node -> 'd Property.t list -> 'i option -> + (node * 'e) list -> unit) -> unit + end module Make(OT : Map.OrderedType) = struct -module Cluster = +module NodeSet = Set.Make(OT) + +module Property = struct - type 'd t = 'd * int - let equal (_,i1) (_,i2) = Int.equal i1 i2 - let compare (_,i1) (_,i2) = Int.compare i1 i2 - let to_string (_,i) = string_of_int i - let data (d,_) = d + type 'd t = { data : 'd; uid : int; having_it : NodeSet.t } + let equal { uid = i1 } { uid = i2 } = Int.equal i1 i2 + let compare { uid = i1 } { uid = i2 } = Int.compare i1 i2 + let to_string { uid = i } = string_of_int i + let data { data = d } = d + let having_it { having_it } = having_it end type node = OT.t module NodeMap = CMap.Make(OT) -module NodeSet = Set.Make(OT) type ('edge,'info,'data) t = { graph : (node * 'edge) list NodeMap.t; - clusters : 'data Cluster.t NodeMap.t; + properties : 'data Property.t list NodeMap.t; infos : 'info NodeMap.t; } let empty = { graph = NodeMap.empty; - clusters = NodeMap.empty; + properties = NodeMap.empty; infos = NodeMap.empty; } @@ -94,7 +97,7 @@ let del_edge dag id tgt = { dag with let del_nodes dag s = { infos = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.infos; - clusters = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.clusters; + properties = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.properties; graph = NodeMap.filter (fun n l -> let drop = NodeSet.mem n s in if not drop then @@ -102,20 +105,31 @@ let del_nodes dag s = { not drop) dag.graph } +let map_add_list k v m = + try + let l = NodeMap.find k m in + NodeMap.add k (v::l) m + with Not_found -> NodeMap.add k [v] m + let clid = ref 1 -let create_cluster dag l data = +let create_property dag l data = incr clid; - { dag with clusters = - List.fold_right (fun x clusters -> - NodeMap.add x (data, !clid) clusters) l dag.clusters } - -let cluster_of dag id = - try Some (NodeMap.find id dag.clusters) - with Not_found -> None - -let del_cluster dag c = - { dag with clusters = - NodeMap.filter (fun _ c' -> not (Cluster.equal c' c)) dag.clusters } + let having_it = List.fold_right NodeSet.add l NodeSet.empty in + let property = { Property.data; uid = !clid; having_it } in + { dag with properties = + List.fold_right (fun x ps -> map_add_list x property ps) l dag.properties } + +let property_of dag id = + try NodeMap.find id dag.properties + with Not_found -> [] + +let del_property dag c = + { dag with properties = + NodeMap.filter (fun _ cl -> cl <> []) + (NodeMap.map (fun cl -> + List.filter (fun c' -> + not (Property.equal c' c)) cl) + dag.properties) } let get_info dag id = try Some (NodeMap.find id dag.infos) @@ -126,7 +140,7 @@ let set_info dag id info = { dag with infos = NodeMap.add id info dag.infos } let clear_info dag id = { dag with infos = NodeMap.remove id dag.infos } let iter dag f = - NodeMap.iter (fun k v -> f k (cluster_of dag k) (get_info dag k) v) dag.graph + NodeMap.iter (fun k v -> f k (property_of dag k) (get_info dag k) v) dag.graph let all_nodes dag = NodeMap.domain dag.graph diff --git a/stm/dag.mli b/stm/dag.mli index 6b4442df0..e783cd8ee 100644 --- a/stm/dag.mli +++ b/stm/dag.mli @@ -7,19 +7,7 @@ (************************************************************************) module type S = sig - - (* A cluster is just a set of nodes. This set holds some data. - Stm uses this to group nodes contribution to the same proofs and - that can be evaluated asynchronously *) - module Cluster : - sig - type 'd t - val equal : 'd t -> 'd t -> bool - val compare : 'd t -> 'd t -> int - val to_string : 'd t -> string - val data : 'd t -> 'd - end - + type node module NodeSet : Set.S with type elt = node @@ -34,19 +22,35 @@ module type S = sig val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t val all_nodes : ('e,'i,'d) t -> NodeSet.t - val iter : ('e,'i,'d) t -> - (node -> 'd Cluster.t option -> 'i option -> - (node * 'e) list -> unit) -> unit - - val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t - val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option - val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t - val get_info : ('e,'i,'d) t -> node -> 'i option val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t -end + (* A property applies to a set of nodes and holds some data. + Stm uses this feature to group nodes contributing to the same proofs and + to structure proofs in boxes limiting the scope of errors *) + module Property : + sig + type 'd t + val equal : 'd t -> 'd t -> bool + val compare : 'd t -> 'd t -> int + val to_string : 'd t -> string + val data : 'd t -> 'd + val having_it : 'd t -> NodeSet.t + end + + val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t + val property_of : ('e,'i,'d) t -> node -> 'd Property.t list + val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t + + val iter : ('e,'i,'d) t -> + (node -> 'd Property.t list -> 'i option -> + (node * 'e) list -> unit) -> unit + + end -module Make(OT : Map.OrderedType) : S with type node = OT.t +module Make(OT : Map.OrderedType) : S +with type node = OT.t +and type NodeSet.t = Set.Make(OT).t +and type NodeSet.elt = OT.t diff --git a/stm/stm.ml b/stm/stm.ml index 1dd089a26..1c8603f0f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -140,7 +140,7 @@ let update_global_env () = if Proof_global.there_are_pending_proofs () then Proof_global.update_global_env () -module Vcs_ = Vcs.Make(Stateid) +module Vcs_ = Vcs.Make(Stateid.Self) type future_proof = Proof_global.closed_proof_output Future.computation type proof_mode = string type depth = int @@ -206,15 +206,28 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *) let default_info () = { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None } +(* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose + * no constraint on properties, here we impose boxes to be non overlapping. *) +type box = + | ProofTask of pt + | ErrorBound of eb +and pt = { (* TODO: inline records in OCaml 4.03 *) + start : Stateid.t; + qed : Stateid.t; +} +and eb = { + stuff : unit; +} + (* Functions that work on a Vcs with a specific branch type *) module Vcs_aux : sig - val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int + val proof_nesting : (branch_type, 't,'i,'c) Vcs_.t -> int val find_proof_at_depth : - (branch_type, 't, 'i) Vcs_.t -> int -> + (branch_type, 't, 'i,'c) Vcs_.t -> int -> Vcs_.Branch.t * branch_type Vcs_.branch_info exception Expired - val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit + val visit : (branch_type, transaction,'i,'c) Vcs_.t -> Vcs_.Dag.node -> visit end = struct (* {{{ *) @@ -278,7 +291,7 @@ module VCS : sig pos : id; } - type vcs = (branch_type, transaction, vcs state_info) Vcs_.t + type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t val init : id -> unit @@ -296,7 +309,7 @@ module VCS : sig val edit_branch : Branch.t val branch : ?root:id -> ?pos:id -> Branch.t -> branch_type -> unit val reset_branch : Branch.t -> id -> unit - val reachable : id -> Vcs_.NodeSet.t + val reachable : id -> Stateid.Set.t val cur_tip : unit -> id val get_info : id -> vcs state_info @@ -309,9 +322,11 @@ module VCS : sig val slice : start:id -> stop:id -> vcs val nodes_in_slice : start:id -> stop:id -> Stateid.t list - val create_cluster : id list -> qed:id -> start:id -> unit - val cluster_of : id -> (id * id) option - val delete_cluster_of : id -> unit + val create_proof_task_box : id list -> qed:id -> start:id -> unit + val create_error_bound_box : id list -> switch:id -> unit + val box_of : id -> box list + val delete_proof_task_box_of : id -> unit + val proof_task_box_of : id -> pt option val proof_nesting : unit -> int val checkout_shallowest_proof_branch : unit -> unit @@ -331,7 +346,6 @@ end = struct (* {{{ *) include Vcs_ exception Expired = Vcs_aux.Expired - module StateidSet = Set.Make(Stateid) open Printf let print_dag vcs () = @@ -373,8 +387,6 @@ end = struct (* {{{ *) let edge tr = sprintf "<%s>" (quote (string_of_transaction tr)) in - let ids = ref StateidSet.empty in - let clus = Hashtbl.create 13 in let node_info id = match get_info vcs id with | None -> "" @@ -387,39 +399,66 @@ end = struct (* {{{ *) let nodefmt oc id = fprintf oc "%s [label=%s,style=filled,fillcolor=%s];\n" (node id) (node_info id) (color id) in - let add_to_clus_or_ids from cf = - match cf with - | None -> ids := StateidSet.add from !ids; false - | Some c -> Hashtbl.replace clus c - (try let n = Hashtbl.find clus c in from::n - with Not_found -> [from]); true in + + let ids = ref Stateid.Set.empty in + let boxes = ref [] in + (* Fill in *) + Dag.iter graph (fun from _ _ l -> + ids := Stateid.Set.add from !ids; + List.iter (fun box -> boxes := box :: !boxes) + (Dag.property_of graph from); + List.iter (fun (dest, _) -> + ids := Stateid.Set.add dest !ids; + List.iter (fun box -> boxes := box :: !boxes) + (Dag.property_of graph dest)) + l); + boxes := CList.sort_uniquize Dag.Property.compare !boxes; + let oc = open_out fname_dot in output_string oc "digraph states {\n"; Dag.iter graph (fun from cf _ l -> - let c1 = add_to_clus_or_ids from cf in List.iter (fun (dest, trans) -> - let c2 = add_to_clus_or_ids dest (Dag.cluster_of graph dest) in - fprintf oc "%s -> %s [xlabel=%s,labelfloat=%b];\n" - (node from) (node dest) (edge trans) (c1 && c2)) l + fprintf oc "%s -> %s [xlabel=%s,labelfloat=true];\n" + (node from) (node dest) (edge trans)) l ); - StateidSet.iter (nodefmt oc) !ids; - Hashtbl.iter (fun c nodes -> - fprintf oc "subgraph cluster_%s {\n" (Dag.Cluster.to_string c); - List.iter (nodefmt oc) nodes; - fprintf oc "color=blue; }\n" - ) clus; + + let contains b1 b2 = + Stateid.Set.subset + (Dag.Property.having_it b2) (Dag.Property.having_it b1) in + let same_box = Dag.Property.equal in + let outerboxes boxes = + List.filter (fun b -> + not (List.exists (fun b1 -> + not (same_box b1 b) && contains b1 b) boxes) + ) boxes in + let rec rec_print b = + boxes := CList.remove same_box b !boxes; + let sub_boxes = List.filter (contains b) (outerboxes !boxes) in + fprintf oc "subgraph cluster_%s {\n" (Dag.Property.to_string b); + List.iter rec_print sub_boxes; + Stateid.Set.iter (fun id -> + if Stateid.Set.mem id !ids then begin + ids := Stateid.Set.remove id !ids; + nodefmt oc id + end) + (Dag.Property.having_it b); + fprintf oc "color=blue; }\n" in + List.iter rec_print (outerboxes !boxes); + Stateid.Set.iter (nodefmt oc) !ids; + List.iteri (fun i (b,id) -> let shape = if Branch.equal head b then "box3d" else "box" in fprintf oc "b%d -> %s;\n" i (node id); fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape (Branch.to_string b); ) heads; + output_string oc "}\n"; close_out oc; ignore(Sys.command ("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps)) - type vcs = (branch_type, transaction, vcs state_info) t + type vcs = (branch_type, transaction, vcs state_info, box) t let vcs : vcs ref = ref (empty Stateid.dummy) let init id = @@ -535,15 +574,39 @@ end = struct (* {{{ *) let nodes_in_slice ~start ~stop = List.rev (List.map fst (nodes_in_slice ~start ~stop)) - let create_cluster l ~qed ~start = vcs := create_cluster !vcs l (qed,start) - let cluster_of id = Option.map Dag.Cluster.data (cluster_of !vcs id) - let delete_cluster_of id = - Option.iter (fun x -> vcs := delete_cluster !vcs x) (Vcs_.cluster_of !vcs id) + let topo_invariant l = + let all = List.fold_right Stateid.Set.add l Stateid.Set.empty in + List.for_all + (fun x -> + let props = property_of !vcs x in + let sets = List.map Dag.Property.having_it props in + List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets) + l + + let create_proof_task_box l ~qed ~start = + if not (topo_invariant l) then anomaly (str "overlapping boxes"); + vcs := create_property !vcs l (ProofTask { qed; start }) + let create_error_bound_box l ~switch = + vcs := create_property !vcs l + (ErrorBound { stuff = () }) + let box_of id = List.map Dag.Property.data (property_of !vcs id) + let delete_proof_task_box_of id = + List.iter (fun x -> vcs := delete_property !vcs x) + (List.filter (fun x -> + match Dag.Property.data x with ProofTask _ -> true | _ -> false) + (Vcs_.property_of !vcs id)) + let proof_task_box_of id = + match + CList.map_filter (function ProofTask x -> Some x | _ -> None) (box_of id) + with + | [] -> None + | [x] -> Some x + | _ -> anomaly (str "node with more than 1 proof task box") let gc () = let old_vcs = !vcs in let new_vcs, erased_nodes = gc old_vcs in - Vcs_.NodeSet.iter (fun id -> + Stateid.Set.iter (fun id -> match (Vcs_aux.visit old_vcs id).step with | `Qed ({ fproof = Some (_, cancel_switch) }, _) | `Cmd { cqueue = `TacQueue cancel_switch } @@ -1878,7 +1941,7 @@ let known_state ?(redefine_qed=false) ~cache id = let drop_pt = keep == VtKeepAsAxiom in let stop, exn_info, loc = eop, (id, eop), x.loc in log_processing_async id name; - VCS.create_cluster nodes ~qed:id ~start; + VCS.create_proof_task_box nodes ~qed:id ~start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> @@ -2403,7 +2466,7 @@ let edit_at id = | _ -> assert false in let is_ancestor_of_cur_branch id = - Vcs_.NodeSet.mem id + Stateid.Set.mem id (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in let has_failed qed_id = match VCS.visit qed_id with @@ -2418,13 +2481,13 @@ let edit_at id = | { next } -> master_for_br root next in let reopen_branch start at_id mode qed_id tip old_branch = let master_id, cancel_switch, keep = - (* Hum, this should be the real start_id in the clusted and not next *) + (* Hum, this should be the real start_id in the cluster and not next *) match VCS.visit qed_id with | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep - | _ -> anomaly (str "Cluster not ending with Qed") in + | _ -> anomaly (str "ProofTask not ending with Qed") in VCS.branch ~root:master_id ~pos:id VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch)); - VCS.delete_cluster_of id; + VCS.delete_proof_task_box_of id; cancel_switch := true; Reach.known_state ~cache:(interactive ()) id; VCS.checkout_shallowest_proof_branch (); @@ -2438,14 +2501,14 @@ let edit_at id = let { mine = brname, brinfo; others } = Backtrack.branches_of id in List.iter (fun (name,{ VCS.kind = k; root; pos }) -> if not(VCS.Branch.equal name VCS.Branch.master) && - Vcs_.NodeSet.mem root ancestors then + Stateid.Set.mem root ancestors then VCS.branch ~root ~pos name k) others; VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id); VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos (Option.default brname bn) (no_edit brinfo.VCS.kind); - VCS.delete_cluster_of id; + VCS.delete_proof_task_box_of id; VCS.gc (); VCS.print (); if not !Flags.async_proofs_full then @@ -2460,14 +2523,14 @@ let edit_at id = | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn) | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn) | _ -> None in - match focused, VCS.cluster_of id, branch_info with + match focused, VCS.proof_task_box_of id, branch_info with | _, Some _, None -> assert false - | false, Some (qed_id,start), Some(mode,bn) -> + | false, Some { qed = qed_id ; start }, Some(mode,bn) -> let tip = VCS.cur_tip () in if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch then reopen_branch start id mode qed_id tip bn else backto id (Some bn) - | true, Some (qed_id,_), Some(mode,bn) -> + | true, Some { qed = qed_id }, Some(mode,bn) -> if on_cur_branch id then begin assert false end else if is_ancestor_of_cur_branch id then begin diff --git a/stm/vcs.ml b/stm/vcs.ml index 38c029901..c483ea4a9 100644 --- a/stm/vcs.ml +++ b/stm/vcs.ml @@ -22,51 +22,49 @@ module type S = sig 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 + + type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ] + + val empty : id -> ('kind,'diff,'info,'property_data) t + + val current_branch : ('k,'e,'i,'c) t -> Branch.t + val branches : ('k,'e,'i,'c) t -> Branch.t list + + val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info + val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) 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 + ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id -> + Branch.t -> 'kind -> ('kind,'e,'i,'c) t + val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) 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 + ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> + Branch.t -> ('k,'diff,'i,'c) t + val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) 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 + ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id -> + Branch.t -> ('k,'diff,'i,'c) t + val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t - 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 + val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t + val get_info : ('k,'e,'info,'c) t -> id -> 'info option + (* Read only dag *) module Dag : Dag.S with type node = id - val dag : ('kind,'diff,'info) t -> ('diff,'info,id*id) Dag.t + val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t + + val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t + val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list + val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) 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 + (* Removes all unreachable nodes and returns them *) + val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t + val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t end @@ -78,7 +76,6 @@ type id = OT.t module NodeSet = Dag.NodeSet - module Branch = struct type t = string @@ -99,10 +96,10 @@ type 'kind branch_info = { pos : id; } -type ('kind,'edge,'info) t = { +type ('kind,'edge,'info,'property_data) t = { cur_branch : Branch.t; heads : 'kind branch_info BranchMap.t; - dag : ('edge,'info,id*id) Dag.t; + dag : ('edge,'info,'property_data) Dag.t; } let empty root = { @@ -167,9 +164,9 @@ 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 create_property vcs l i = { vcs with dag = Dag.create_property vcs.dag l i } +let property_of vcs i = Dag.property_of vcs.dag i +let delete_property vcs c = { vcs with dag = Dag.del_property vcs.dag c } let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads [] let dag vcs = vcs.dag diff --git a/stm/vcs.mli b/stm/vcs.mli index 8f22fee84..46b40f8a4 100644 --- a/stm/vcs.mli +++ b/stm/vcs.mli @@ -19,10 +19,11 @@ As a consequence, "checkout" just updates the current branch. The type [id] is the type of commits (a node in the dag) - The type [Vcs.t] has 3 parameters: + The type [Vcs.t] has 4 parameters: ['info] data attached to a node (like a system state) ['diff] data attached to an edge (the commit content, a "patch") ['kind] extra data attached to a branch (like being the master branch) + ['cdata] extra data hold by dag properties *) module type S = sig @@ -45,46 +46,51 @@ module type S = sig pos : id; } - type ('kind,'diff,'info) t constraint 'kind = [> `Master ] + type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ] - val empty : id -> ('kind,'diff,'info) t + val empty : id -> ('kind,'diff,'info,'property_data) t - val current_branch : ('k,'e,'i) t -> Branch.t - val branches : ('k,'e,'i) t -> Branch.t list + val current_branch : ('k,'e,'i,'c) t -> Branch.t + val branches : ('k,'e,'i,'c) 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 get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info + val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) 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 + ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id -> + Branch.t -> 'kind -> ('kind,'e,'i,'c) t + val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) 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 + ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> + Branch.t -> ('k,'diff,'i,'c) t + val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) 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 + ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id -> + Branch.t -> ('k,'diff,'i,'c) t + val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t - val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t - val get_info : ('k,'e,'info) t -> id -> 'info option + val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t + val get_info : ('k,'e,'info,'c) t -> id -> 'info option - module NodeSet : Set.S with type elt = id + (* Read only dag *) + module Dag : Dag.S with type node = id + val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t - (* Removes all unreachable nodes and returns them *) - val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t + (* Properties are not a concept typical of a VCS, but a useful metadata + * of a DAG (or graph). *) + val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t + val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list + val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t - val reachable : ('k,'e,'info) t -> id -> NodeSet.t + (* Removes all unreachable nodes and returns them *) + val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t + val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t - (* read only dag *) - 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) : S with type id = OT.t +module Make(OT : Map.OrderedType) : S +with type id = OT.t +and type Dag.node = OT.t +and type Dag.NodeSet.t = Set.Make(OT).t +and type Dag.NodeSet.elt = OT.t + -- cgit v1.2.3