Use a single search function.

We use the search function that maintains a maximum scope during traversal.
The other search function is removed.
This commit is contained in:
Olivier 2023-02-23 10:10:59 +01:00
parent 905c703eb8
commit d1f3c5f55f
1 changed files with 22 additions and 46 deletions

View File

@ -131,52 +131,16 @@ end = struct
| _ ->
List.map Option.get vs
(* TODO : use a mark to keep trace of already visited vertices like in
[data] ? *)
let rec search
(stop:vertex -> bool) (v:vertex) (visited:vertex list)
: vertex option =
if stop v then
Some v
else
let neighbours = List.map fst (get_neighbours v) in
let unvisited_neighbours =
List.filter (fun v -> not (List.mem v visited)) neighbours
in
List.fold_left (fun res v ->
match res with
| None ->
search stop v (v::visited)
| Some _ ->
res
) None unvisited_neighbours
let search stop v =
search stop v []
let path_exists v1 v2 =
assert (StructTable.mem table v1);
assert (StructTable.mem table v2);
let stop =
( = ) v2
in
match search stop v1 with
| None ->
false
| Some _ ->
true
(* We added edges to represent equalities only when necessary. So we have the
property that there is at most one path between two vertices. Hence
we know that the biggest scope encountered along the path between two
vertices is the lowest scope where the equality is well-defined. *)
(* By relying on this property, [search_scope stop vs] makes a depth-first
search through the graph, stopping when the predicate [stop] become true.
It maintains a worklist of nodes to visit, with a maximum scope associate
encountered along the way. *)
let rec search_scope (stop : vertex -> bool) (vs : (vertex * scope) list)
(* By relying on this property, [search stop vs visited] makes a depth-first
search through the graph, stopping when the predicate [stop] becomes true.
It maintains a worklist of nodes to visit, each associated with a maximum
scope encountered along the way, and a list of already visited vertices. *)
let rec search (stop : vertex -> bool) (vs : (vertex * scope) list)
(visited : vertex list)
: (vertex * scope) option =
match vs with
@ -203,10 +167,22 @@ end = struct
) unexplored_neighbours
in
(* ... and call ourselves recursively with the unvisited vertices *)
search_scope stop (neighbours_scope_max @ vs) (v1 :: visited)
search stop (neighbours_scope_max @ vs) (v1 :: visited)
let search_scope stop v1 scope =
search_scope stop [(v1,scope)] []
let search stop v1 scope =
search stop [(v1,scope)] []
let path_exists v1 v2 =
assert (StructTable.mem table v1);
assert (StructTable.mem table v2);
let stop =
( = ) v2
in
match search stop v1 base_scope with
| None ->
false
| Some _ ->
true
let get_structure v : vertex Abs.structure * scope =
assert (StructTable.mem table v);
@ -217,7 +193,7 @@ end = struct
| S (Abs.Abstract _) ->
false
in
match search_scope stop v base_scope with
match search stop v base_scope with
| None ->
(* If the vertex is not connected to a structure return itself
(an abstract structure).
@ -342,7 +318,7 @@ end = struct
false
in
(* Returns only the scope. *)
Option.map snd @@ search_scope stop v1 base_scope
Option.map snd @@ search stop v1 base_scope
end (* EqEnv *)