Topological sort: Difference between revisions

Content added Content deleted
Line 526: Line 526:
in
in


abstype marks_t (n : int)
abstype marks (n : int)
assume marks_t n = _marksvec_t n
assume marks n = _marksvec_t n


fn marks_t_make_elt
fn marks_make_elt
{n : nat}
{n : nat}
{b : int | b == 0 || b == 1}
{b : int | b == 0 || b == 1}
Line 538: Line 538:


fn
fn
marks_set_at
marks_t_set_at
{n : int}
{n : int}
{i : nat | i < n}
{i : nat | i < n}
Line 549: Line 549:


fn
fn
marks_get_at
marks_t_get_at
{n : int}
{n : int}
{i : nat | i < n}
{i : nat | i < n}
Line 559: Line 559:


fn
fn
marks_setall
marks_t_setall
{n : int}
{n : int}
{b : int | b == 0 || b == 1}
{b : int | b == 0 || b == 1}
Line 577: Line 577:
end
end


overload [] with marks_t_set_at of 100
overload [] with marks_set_at of 100
overload [] with marks_t_get_at of 100
overload [] with marks_get_at of 100
overload setall with marks_t_setall of 100
overload setall with marks_setall of 100


end
end
Line 592: Line 592:
entries of each sublist forms the list of dependencies of the first
entries of each sublist forms the list of dependencies of the first
entry. Thus this is a kind of association list. *)
entry. Thus this is a kind of association list. *)
typedef depdesc_t (n : int) = list (List1 String1, n)
typedef depdesc (n : int) = list (List1 String1, n)
typedef depdesc_t = [n : nat] depdesc_t n
typedef depdesc = [n : nat] depdesc n


typedef char_skipper_t =
typedef char_skipper =
{n : int}
{n : int}
{i : nat | i <= n}
{i : nat | i <= n}
Line 607: Line 607:
make_char_skipper
make_char_skipper
(match : char -<> bool)
(match : char -<> bool)
:<> char_skipper_t =
:<> char_skipper =
let
let
fun
fun
Line 679: Line 679:
i : size_t i)
i : size_t i)
:<!wrt> [j : int | i <= j; j <= n]
:<!wrt> [j : int | i <= j; j <= n]
@(depdesc_t, size_t j) =
@(depdesc, size_t j) =
let
let
fun
fun
loop {i : nat | i <= n}
loop {i : nat | i <= n}
.<n - i>.
.<n - i>.
(desc : depdesc_t,
(desc : depdesc,
i : size_t i)
i : size_t i)
:<!wrt> [j : int | i <= j; j <= n]
:<!wrt> [j : int | i <= j; j <= n]
@(depdesc_t, size_t j) =
@(depdesc, size_t j) =
let
let
val i = skip_spaces (text, n, i)
val i = skip_spaces (text, n, i)
Line 732: Line 732:
fn
fn
read_depdesc ()
read_depdesc ()
: depdesc_t =
: depdesc =
let
let
val text = read_to_string ()
val text = read_to_string ()
Line 747: Line 747:


(* An ordered list of the node names. *)
(* An ordered list of the node names. *)
typedef nodenames_t (n : int) = list (String1, n)
typedef nodenames (n : int) = list (String1, n)


(* A more efficient representation for nodes: integers in 0..n. *)
(* A more efficient representation for nodes: integers in 0..n. *)
typedef nodenum_t (n : int) = [num : nat | num <= n - 1] size_t num
typedef nodenum (n : int) = [num : nat | num <= n - 1] size_t num


(* A collection of directed edges. *)
(* A collection of directed edges. *)
typedef edges_t (n : int) = arrayref (List0 (nodenum_t n), n)
typedef edges (n : int) = arrayref (List0 (nodenum n), n)


(* An internal representation of data for a topological sort. *)
(* An internal representation of data for a topological sort. *)
typedef toposort_t (n : int) =
typedef topodata (n : int) =
'{
'{
n = size_t n, (* The number of nodes. *)
n = size_t n, (* The number of nodes. *)
edges = edges_t n, (* Directed edges. *)
edges = edges n, (* Directed edges. *)
tempmarks = marks_t n, (* Temporary marks. *)
tempmarks = marks n, (* Temporary marks. *)
permmarks = marks_t n (* Permanent marks. *)
permmarks = marks n (* Permanent marks. *)
}
}


fn
fn
collect_nodenames
collect_nodenames
(desc : depdesc_t)
(desc : depdesc)
:<!wrt> [n : nat]
:<!wrt> [n : nat]
@(nodenames_t n,
@(nodenames n,
size_t n) =
size_t n) =
let
let
Line 777: Line 777:
.<m>.
.<m>.
(row : list (String1, m),
(row : list (String1, m),
names : &nodenames_t n0 >> nodenames_t n1,
names : &nodenames n0 >> nodenames n1,
n : &size_t n0 >> size_t n1)
n : &size_t n0 >> size_t n1)
:<!wrt> #[n1 : int | n0 <= n1]
:<!wrt> #[n1 : int | n0 <= n1]
Line 802: Line 802:
.<m>.
.<m>.
(desc : list (List1 String1, m),
(desc : list (List1 String1, m),
names : &nodenames_t n0 >> nodenames_t n1,
names : &nodenames n0 >> nodenames n1,
n : &size_t n0 >> size_t n1)
n : &size_t n0 >> size_t n1)
:<!wrt> #[n1 : int | n0 <= n1]
:<!wrt> #[n1 : int | n0 <= n1]
Line 824: Line 824:
nodename_number
nodename_number
{n : int}
{n : int}
(nodenames : nodenames_t n,
(nodenames : nodenames n,
name : String1)
name : String1)
:<> Option (nodenum_t n) =
:<> Option (nodenum n) =
let
let
fun
fun
loop {i : nat | i <= n}
loop {i : nat | i <= n}
.<n - i>.
.<n - i>.
(names : nodenames_t (n - i),
(names : nodenames (n - i),
i : size_t i)
i : size_t i)
:<> Option (nodenum_t n) =
:<> Option (nodenum n) =
case+ names of
case+ names of
| NIL => None ()
| NIL => None ()
Line 849: Line 849:
fn
fn
add_edge {n : int}
add_edge {n : int}
(edges : edges_t n,
(edges : edges n,
from : nodenum_t n,
from : nodenum n,
to : nodenum_t n)
to : nodenum n)
:<!refwrt> void =
:<!refwrt> void =
(* This implementation does not store duplicate edges. *)
(* This implementation does not store duplicate edges. *)
let
let
val old_edges = edges[from]
val old_edges = edges[from]
implement list_find$pred<nodenum_t n> s = (s = to)
implement list_find$pred<nodenum n> s = (s = to)
in
in
case+ list_find_opt<nodenum_t n> old_edges of
case+ list_find_opt<nodenum n> old_edges of
| ~ None_vt () => edges[from] := to :: old_edges
| ~ None_vt () => edges[from] := to :: old_edges
| ~ Some_vt _ => ()
| ~ Some_vt _ => ()
Line 867: Line 867:
{n : int}
{n : int}
{m : int}
{m : int}
(edges : edges_t n,
(edges : edges n,
n : size_t n,
n : size_t n,
desc : depdesc_t m,
desc : depdesc m,
nodenames : nodenames_t n)
nodenames : nodenames n)
:<!refwrt> void =
:<!refwrt> void =
let
let
Line 893: Line 893:
{m1 : nat}
{m1 : nat}
.<m1>.
.<m1>.
(headnum : nodenum_t n,
(headnum : nodenum n,
lst : list (String1, m1))
lst : list (String1, m1))
:<!refwrt> void =
:<!refwrt> void =
Line 929: Line 929:


fn
fn
topodata_make
toposort_t_make
(desc : depdesc_t)
(desc : depdesc)
:<!refwrt> [n : nat]
:<!refwrt> [n : nat]
@(toposort_t n,
@(topodata n,
nodenames_t n) =
nodenames n) =
let
let
val @(nodenames, n) = collect_nodenames desc
val @(nodenames, n) = collect_nodenames desc
Line 939: Line 939:
prval [n : int] EQINT () = eqint_make_guint n
prval [n : int] EQINT () = eqint_make_guint n


val edges = arrayref_make_elt<List0 (nodenum_t n)> (n, NIL)
val edges = arrayref_make_elt<List0 (nodenum n)> (n, NIL)
val () = fill_edges {n} (edges, n, desc, nodenames)
val () = fill_edges {n} (edges, n, desc, nodenames)


val tempmarks = marks_t_make_elt (n, 0)
val tempmarks = marks_make_elt (n, 0)
and permmarks = marks_t_make_elt (n, 0)
and permmarks = marks_make_elt (n, 0)


val topo =
val topo =
Line 963: Line 963:


*)
*)

(* What return values are made from. *)
datatype toporesult (a : t@ype, n : int) =
| {0 <= n}
Topo_SUCCESS (a, n) of list (a, n)
| Topo_CYCLE (a, n) of List1 a
typedef toporesult (a : t@ype) = [n : int] toporesult (a, n)


fn
fn
find_unmarked_node
find_unmarked_node
{n : int}
{n : int}
(topo : toposort_t n)
(topo : topodata n)
:<!ref> Option (nodenum_t n) =
:<!ref> Option (nodenum n) =
let
let
val n = topo.n
val n = topo.n
Line 979: Line 986:
.<n - i>.
.<n - i>.
(i : size_t i)
(i : size_t i)
:<!ref> Option (nodenum_t n) =
:<!ref> Option (nodenum n) =
if i = n then
if i = n then
None ()
None ()
Line 992: Line 999:
fun
fun
visit {n : int}
visit {n : int}
(topo : toposort_t n,
(topo : topodata n,
nodenum : nodenum_t n,
nodenum : nodenum n,
accum : List0 (nodenum_t n))
accum : List0 (nodenum n),
:<!ntm,!refwrt> Option (List0 (nodenum_t n)) =
path : List0 (nodenum n))
: toporesult (nodenum n) =
(* Probably it is cumbersome to include a proof this routine
(* Probably it is cumbersome to include a proof this routine
terminates. Thus I will not try to include one. *)
terminates. Thus I will not try to write one. *)
let
let
val edges = topo.edges
val n = topo.n
and edges = topo.edges
and tempmarks = topo.tempmarks
and tempmarks = topo.tempmarks
and permmarks = topo.permmarks
and permmarks = topo.permmarks
in
in
if permmarks[nodenum] = 1 then
if permmarks[nodenum] = 1 then
Some accum
Topo_SUCCESS accum
else if tempmarks[nodenum] = 1 then
else if tempmarks[nodenum] = 1 then
None ()
let
val () = assertloc (isneqz path)
⚫
in
Topo_CYCLE (list_vt2t (reverse path))
⚫
end
else
else
let
let
Line 1,013: Line 1,026:
{k : nat}
{k : nat}
.<k>.
.<k>.
(topo : toposort_t n,
(topo : topodata n,
to_visit : list (nodenum_t n, k),
to_visit : list (nodenum n, k),
accum : List0 (nodenum_t n))
accum : List0 (nodenum n),
:<!ntm,!refwrt> Option (List0 (nodenum_t n)) =
path : List0 (nodenum n))
: toporesult (nodenum n) =
case+ to_visit of
case+ to_visit of
| NIL => Some accum
| NIL => Topo_SUCCESS accum
| node_to_visit :: tail =>
| node_to_visit :: tail =>
begin
begin
case+ visit (topo, node_to_visit, accum) of
case+ visit (topo, node_to_visit, accum, path) of
| None () => None ()
| Topo_SUCCESS accum1 =>
| Some accum1 => recursive_visits (topo, tail, accum1)
recursive_visits (topo, tail, accum1, path)
| other => other
end
end
in
in
tempmarks[nodenum] := 1;
tempmarks[nodenum] := 1;
case+ recursive_visits (topo, edges[nodenum], accum) of
case+ recursive_visits (topo, edges[nodenum], accum,
| None () => None ()
nodenum :: path) of
| Some accum1 =>
| Topo_SUCCESS accum1 =>
begin
begin
tempmarks[nodenum] := 0;
tempmarks[nodenum] := 0;
permmarks[nodenum] := 1;
permmarks[nodenum] := 1;
Some (nodenum :: accum1)
Topo_SUCCESS (nodenum :: accum1)
end
end
| other => other
end
end
end
end
Line 1,041: Line 1,057:
topological_sort
topological_sort
{n : int}
{n : int}
(topo : toposort_t n)
(topo : topodata n)
: toporesult (nodenum n, n) =
(* I do not bother to try to restrict effects. *)
: Option (list (nodenum_t n, n)) =
let
let
prval () = lemma_arrayref_param (topo.edges)
prval () = lemma_arrayref_param (topo.edges)


fun
fun
sort (accum : List0 (nodenum_t n))
sort (accum : List0 (nodenum n))
: Option (list (nodenum_t n, n)) =
: toporesult (nodenum n, n) =
case+ find_unmarked_node topo of
case+ find_unmarked_node topo of
| None () =>
| None () =>
Line 1,056: Line 1,071:
val () = assertloc (i2sz (length accum) = topo.n)
val () = assertloc (i2sz (length accum) = topo.n)
in
in
Some accum
Topo_SUCCESS accum
end
end
| Some nodenum =>
| Some nodenum =>
begin
begin
case+ visit (topo, nodenum, accum) of
case+ visit (topo, nodenum, accum, NIL) of
| None () => None ()
| Topo_SUCCESS accum1 => sort accum1
| Some accum1 => sort accum1
| Topo_CYCLE cycle => Topo_CYCLE cycle
end
end


Line 1,081: Line 1,096:
fn
fn
find_a_valid_order
find_a_valid_order
(desc : depdesc_t)
(desc : depdesc)
⚫
: toporesult String1 =
(* I do not bother to try to restrict effects. *)
⚫
: Option (List0 String1) =
let
let
val @(topo, nodenames) = toposort_t_make desc
val @(topo, nodenames) = topodata_make desc

in
⚫
prval [n : int] EQINT () = eqint_make_guint (topo.n)
⚫
case+ topological_sort topo of
| None () => None ()
⚫
| Some valid_order =>
⚫
let
⚫
val nodenames_array =
⚫
arrayref_make_list<String1> (sz2i (topo.n), nodenames)


⚫
val nodenames_array =
⚫
prval [n : int] EQINT () = eqint_make_guint (topo.n)
⚫
arrayref_make_list<String1> (sz2i (topo.n), nodenames)


implement
implement
list_map$fopr<nodenum_t n><String1> i =
list_map$fopr<nodenum n><String1> i =
nodenames_array[i]
nodenames_array[i]

⚫
in
Some (list_vt2t (list_map<nodenum_t n><String1> valid_order))
macdef map = list_map<nodenum n><String1>
end
in
⚫
case+ topological_sort topo of
⚫
| Topo_SUCCESS valid_order =>
Topo_SUCCESS (list_vt2t (map valid_order))
| Topo_CYCLE cycle =>
Topo_CYCLE (list_vt2t (map cycle))
end
end


Line 1,112: Line 1,127:
in
in
case+ find_a_valid_order desc of
case+ find_a_valid_order desc of
| Topo_SUCCESS valid_order =>
| None () => println! "**** dependency loop ****"
| Some valid_order => println! (valid_order : List0 string)
println! (valid_order : List0 string)
| Topo_CYCLE cycle =>
let
val last = list_last cycle
val cycl = list_vt2t (reverse (last :: cycle))
⚫
in
println! ("COMPILATION CYCLE: ", cycl : List0 string)
end
end
end


Line 1,142: Line 1,164:
ieee, dware, dw05, dw06, dw07, gtech, dw01, dw04, dw02, std_cell_lib, synopsys, std, dw03, ramlib, des_system_lib
ieee, dware, dw05, dw06, dw07, gtech, dw01, dw04, dw02, std_cell_lib, synopsys, std, dw03, ramlib, des_system_lib
</pre>
</pre>

AND ...


Data fed to standard input:
Data fed to standard input:
<pre>
<pre>
a b; b d; d a e; e a;
des_system_lib std synopsys std_cell_lib des_system_lib dw02 dw01 ramlib ieee;
dw01 ieee dw01 dware gtech dw04;
dw02 ieee dw02 dware;
dw03 std synopsys dware dw03 dw02 dw01 ieee gtech;
dw04 dw04 ieee dw01 dware gtech;
dw05 dw05 ieee dware;
dw06 dw06 ieee dware;
dw07 ieee dware;
dware ieee dware;
gtech ieee gtech;
ramlib std ieee;
std_cell_lib ieee std_cell_lib;
synopsys;
</pre>
</pre>


Data from standard output:
Data from standard output:
<pre>
<pre>
COMPILATION CYCLE: b, d, e, a, b
**** dependency loop ****
</pre>
</pre>

''Note: I plan to enhance the function to return information about the cyclic dependency, rather than simply "None()".''


=={{header|Bracmat}}==
=={{header|Bracmat}}==
Retrieved from "https://rosettacode.org/wiki/Topological_sort"