diff options
| -rw-r--r-- | lib/acyclicGraph.ml | 171 |
1 files changed, 124 insertions, 47 deletions
diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml index 14c08da35d..17299c72eb 100644 --- a/lib/acyclicGraph.ml +++ b/lib/acyclicGraph.ml @@ -58,15 +58,59 @@ module Make (Point:Point) = struct *) - module PMap = Point.Map - module PSet = Point.Set + module Index : + sig + type t + val equal : t -> t -> bool + module Set : CSig.SetS with type elt = t + module Map : CMap.ExtS with type key = t and module Set := Set + type table + val empty : table + val fresh : Point.t -> table -> t * table + val mem : Point.t -> table -> bool + val find : Point.t -> table -> t + val repr : t -> table -> Point.t + end = + struct + type t = int + let equal = Int.equal + module Set = Int.Set + module Map = Int.Map + + type table = { + tab_len : int; + tab_fwd : Point.t Int.Map.t; + tab_bwd : int Point.Map.t + } + + let empty = { + tab_len = 0; + tab_fwd = Int.Map.empty; + tab_bwd = Point.Map.empty; + } + let mem x t = Point.Map.mem x t.tab_bwd + let find x t = Point.Map.find x t.tab_bwd + let repr n t = Int.Map.find n t.tab_fwd + + let fresh x t = + let () = assert (not @@ mem x t) in + let n = t.tab_len in + n, { + tab_len = n + 1; + tab_fwd = Int.Map.add n x t.tab_fwd; + tab_bwd = Point.Map.add x n t.tab_bwd; + } + end + + module PMap = Index.Map + module PSet = Index.Set module Constraint = Point.Constraint type status = NoMark | Visited | WeakVisited | ToMerge (* Comparison on this type is pointer equality *) type canonical_node = - { canon: Point.t; + { canon: Index.t; ltle: bool PMap.t; (* true: strict (lt) constraint. false: weak (le) constraint. *) gtge: PSet.t; @@ -81,12 +125,13 @@ module Make (Point:Point) = struct type entry = | Canonical of canonical_node - | Equiv of Point.t + | Equiv of Index.t type t = { entries : entry PMap.t; index : int; - n_nodes : int; n_edges : int } + n_nodes : int; n_edges : int; + table : Index.table } (** Used to cleanup mutable marks if a traversal function is interrupted before it has the opportunity to do it itself. *) @@ -121,7 +166,8 @@ module Make (Point:Point) = struct | _ -> assert false) g.entries; index = g.index; n_nodes = g.n_nodes - 1; - n_edges = g.n_edges } + n_edges = g.n_edges; + table = g.table } (* Low-level function : changes data associated with a canonical node. Resets the mutable fields in the old record, in order to avoid breaking @@ -145,7 +191,10 @@ module Make (Point:Point) = struct | Canonical arc -> arc | exception Not_found -> CErrors.anomaly ~label:"Univ.repr" - Pp.(str"Universe " ++ Point.pr u ++ str" undefined.") + Pp.(str"Universe " ++ Point.pr (Index.repr u g.table) ++ str" undefined.") + + let repr_node g u = + repr g (Index.find u g.table) exception AlreadyDeclared @@ -168,6 +217,7 @@ module Make (Point:Point) = struct (* Checks most of the invariants of the graph. For debugging purposes. *) let check_invariants ~required_canonical g = + let required_canonical u = required_canonical (Index.repr u g.table) in let n_edges = ref 0 in let n_nodes = ref 0 in PMap.iter (fun l u -> @@ -188,7 +238,7 @@ module Make (Point:Point) = struct PMap.exists (fun l _ -> u == repr g l) v.ltle)) ) u.gtge; assert (u.status = NoMark); - assert (Point.equal l u.canon); + assert (Index.equal l u.canon); assert (u.ilvl > g.index); assert (not (PMap.mem u.canon u.ltle)); incr n_nodes @@ -200,7 +250,7 @@ module Make (Point:Point) = struct let clean_ltle g ltle = PMap.fold (fun u strict acc -> let uu = (repr g u).canon in - if Point.equal uu u then acc + if Index.equal uu u then acc else ( let acc = PMap.remove u (fst acc) in if not strict && PMap.mem uu acc then (acc, true) @@ -210,7 +260,7 @@ module Make (Point:Point) = struct let clean_gtge g gtge = PSet.fold (fun u acc -> let uu = (repr g u).canon in - if Point.equal uu u then acc + if Index.equal uu u then acc else PSet.add uu (PSet.remove u (fst acc)), true) gtge (gtge, false) @@ -314,7 +364,7 @@ module Make (Point:Point) = struct | Visited -> false, to_revert | ToMerge -> true, to_revert | NoMark -> let to_revert = x::to_revert in - if Point.equal x.canon v then + if Index.equal x.canon v then begin x.status <- ToMerge; true, to_revert end else begin @@ -425,7 +475,7 @@ module Make (Point:Point) = struct (* Inserting shortcuts for old nodes. *) let g = List.fold_left (fun g n -> - if Point.equal n.canon root.canon then g else enter_equiv g n.canon root.canon) + if Index.equal n.canon root.canon then g else enter_equiv g n.canon root.canon) g to_merge in @@ -481,11 +531,10 @@ module Make (Point:Point) = struct raise e let add ?(rank=0) v g = - try - let _arcv = PMap.find v g.entries in - raise AlreadyDeclared - with Not_found -> - assert (g.index > min_int); + if Index.mem v g.table then raise AlreadyDeclared + else + let () = assert (g.index > min_int) in + let v, table = Index.fresh v g.table in let node = { canon = v; ltle = PMap.empty; @@ -497,17 +546,18 @@ module Make (Point:Point) = struct } in let entries = PMap.add v (Canonical node) g.entries in - { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } + { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges; table } exception Undeclared of Point.t let check_declared g us = - let check l = if not (PMap.mem l g.entries) then raise (Undeclared l) in - PSet.iter check us + let check l = if not (Index.mem l g.table) then raise (Undeclared l) in + Point.Set.iter check us exception Found_explanation of (constraint_type * Point.t) list let get_explanation strict u v g = - let v = repr g v in + let u = Index.find u g.table in + let v = repr_node g v in let visited_strict = ref PMap.empty in let rec traverse strict u = if u == v then @@ -527,6 +577,7 @@ module Make (Point:Point) = struct | None -> () | Some exp -> let typ = if strictu' then Lt else Le in + let u' = Index.repr u' g.table in raise (Found_explanation ((typ, u') :: exp))) u.ltle; None @@ -534,7 +585,7 @@ module Make (Point:Point) = struct end in let u = repr g u in - if u == v then [(Eq, v.canon)] + if u == v then [(Eq, Index.repr v.canon g.table)] else match traverse strict u with Some exp -> exp | None -> assert false let get_explanation strict u v g = @@ -608,21 +659,27 @@ module Make (Point:Point) = struct let check_eq g u v = u == v || - let arcu = repr g u and arcv = repr g v in + let arcu = repr_node g u and arcv = repr_node g v in arcu == arcv let check_smaller g strict u v = - search_path strict (repr g u) (repr g v) g + search_path strict (repr_node g u) (repr_node g v) g let check_leq g u v = check_smaller g false u v let check_lt g u v = check_smaller g true u v (* enforce_eq g u v will force u=v if possible, will fail otherwise *) - let rec enforce_eq u v g = - let ucan = repr g u in - let vcan = repr g v in - if topo_compare ucan vcan = 1 then enforce_eq v u g + let enforce_eq u v g = + let ucan = repr_node g u in + let vcan = repr_node g v in + if ucan == vcan then g + else if topo_compare ucan vcan = 1 then + let ucan = vcan and vcan = ucan in + let g = insert_edge false ucan vcan g in (* Cannot fail *) + try insert_edge false vcan ucan g + with CycleDetected -> + Point.error_inconsistency Eq v u (get_explanation true v u g) else let g = insert_edge false ucan vcan g in (* Cannot fail *) try insert_edge false vcan ucan g @@ -631,35 +688,40 @@ module Make (Point:Point) = struct (* enforce_leq g u v will force u<=v if possible, will fail otherwise *) let enforce_leq u v g = - let ucan = repr g u in - let vcan = repr g v in + let ucan = repr_node g u in + let vcan = repr_node g v in try insert_edge false ucan vcan g with CycleDetected -> Point.error_inconsistency Le u v (get_explanation true v u g) (* enforce_lt u v will force u<v if possible, will fail otherwise *) let enforce_lt u v g = - let ucan = repr g u in - let vcan = repr g v in + let ucan = repr_node g u in + let vcan = repr_node g v in try insert_edge true ucan vcan g with CycleDetected -> Point.error_inconsistency Lt u v (get_explanation false v u g) let empty = - { entries = PMap.empty; index = 0; n_nodes = 0; n_edges = 0 } + { entries = PMap.empty; index = 0; n_nodes = 0; n_edges = 0; table = Index.empty } (* Normalization *) let constraints_of g = - let module UF = Unionfind.Make (PSet) (PMap) in + let module UF = Unionfind.Make (Point.Set) (Point.Map) in let uf = UF.create () in let constraints_of u v acc = match v with | Canonical {canon=u; ltle; _} -> PMap.fold (fun v strict acc-> let typ = if strict then Lt else Le in + let u = Index.repr u g.table in + let v = Index.repr v g.table in Constraint.add (u,typ,v) acc) ltle acc - | Equiv v -> UF.union u v uf; acc + | Equiv v -> + let u = Index.repr u g.table in + let v = Index.repr v g.table in + UF.union u v uf; acc in let csts = PMap.fold constraints_of g.entries Constraint.empty in csts, UF.partition uf @@ -667,16 +729,20 @@ module Make (Point:Point) = struct (* domain g.entries = kept + removed *) let constraints_for ~kept g = (* rmap: partial map from canonical points to kept points *) + let add_cst u knd v cst = + Constraint.add (Index.repr u g.table, knd, Index.repr v g.table) cst + in + let kept = Point.Set.fold (fun u accu -> PSet.add (Index.find u g.table) accu) kept PSet.empty in let rmap, csts = PSet.fold (fun u (rmap,csts) -> let arcu = repr g u in if PSet.mem arcu.canon kept then - let csts = if Point.equal u arcu.canon then csts - else Constraint.add (u,Eq,arcu.canon) csts + let csts = if Index.equal u arcu.canon then csts + else add_cst u Eq arcu.canon csts in PMap.add arcu.canon arcu.canon rmap, csts else match PMap.find arcu.canon rmap with - | v -> rmap, Constraint.add (u,Eq,v) csts + | v -> rmap, add_cst u Eq v csts | exception Not_found -> PMap.add arcu.canon u rmap, csts) kept (PMap.empty,Constraint.empty) in @@ -687,7 +753,7 @@ module Make (Point:Point) = struct (match PMap.find v.canon rmap with | v -> let d = if strict then Lt else Le in - let csts = Constraint.add (u,d,v) csts in + let csts = add_cst u d v csts in add_from u csts todo | exception Not_found -> (* v is not equal to any kept point *) @@ -703,18 +769,23 @@ module Make (Point:Point) = struct arc.ltle csts) kept csts - let domain g = PMap.domain g.entries + let domain g = + let fold u _ accu = Point.Set.add (Index.repr u g.table) accu in + PMap.fold fold g.entries Point.Set.empty let choose p g u = let exception Found of Point.t in - let ru = (repr g u).canon in - if p ru then Some ru + let ru = (repr_node g u).canon in + let ruv = Index.repr ru g.table in + if p ruv then Some ruv else try PMap.iter (fun v -> function | Canonical _ -> () (* we already tried [p ru] *) | Equiv v' -> let rv = (repr g v').canon in - if rv == ru && p v then raise (Found v) + if rv == ru then + let v = Index.repr v g.table in + if p v then raise (Found v) (* NB: we could also try [p v'] but it will come up in the rest of the iteration regardless. *) ) g.entries; None @@ -724,10 +795,16 @@ module Make (Point:Point) = struct type repr = node Point.Map.t let repr g = - let map n = match n with - | Canonical n -> Node n.ltle - | Equiv u -> Alias u + let fold u n accu = + let n = match n with + | Canonical n -> + let fold u lt accu = Point.Map.add (Index.repr u g.table) lt accu in + let ltle = PMap.fold fold n.ltle Point.Map.empty in + Node ltle + | Equiv u -> Alias (Index.repr u g.table) + in + Point.Map.add (Index.repr u g.table) n accu in - Point.Map.map map g.entries + PMap.fold fold g.entries Point.Map.empty end |