Rosetta Code

Topological sort: Difference between revisions

Page Discussion

Topological sort (view source)

Revision as of 17:50, 18 October 2022

97 bytes removed ,  1 year ago
→‎{{header|ATS}}
Line 526:
in
 
abstype marks_tmarks (n : int)
assume marks_tmarks n = _marksvec_t n
 
fn marks_t_make_eltmarks_make_elt
{n : nat}
{b : int | b == 0 || b == 1}
Line 538:
 
fn
marks_set_at
marks_t_set_at
{n : int}
{i : nat | i < n}
Line 549:
 
fn
marks_get_at
marks_t_get_at
{n : int}
{i : nat | i < n}
Line 559:
 
fn
marks_setall
marks_t_setall
{n : int}
{b : int | b == 0 || b == 1}
Line 577:
end
 
overload [] with marks_t_set_atmarks_set_at of 100
overload [] with marks_t_get_atmarks_get_at of 100
overload setall with marks_t_setallmarks_setall of 100
 
end
Line 592:
entries of each sublist forms the list of dependencies of the first
entry. Thus this is a kind of association list. *)
typedef depdesc_tdepdesc (n : int) = list (List1 String1, n)
typedef depdesc_tdepdesc = [n : nat] depdesc_tdepdesc n
 
typedef char_skipper_tchar_skipper =
{n : int}
{i : nat | i <= n}
Line 607:
make_char_skipper
(match : char -<> bool)
:<> char_skipper_tchar_skipper =
let
fun
Line 679:
i : size_t i)
:<!wrt> [j : int | i <= j; j <= n]
@(depdesc_tdepdesc, size_t j) =
let
fun
loop {i : nat | i <= n}
.<n - i>.
(desc : depdesc_tdepdesc,
i : size_t i)
:<!wrt> [j : int | i <= j; j <= n]
@(depdesc_tdepdesc, size_t j) =
let
val i = skip_spaces (text, n, i)
Line 732:
fn
read_depdesc ()
: depdesc_tdepdesc =
let
val text = read_to_string ()
Line 747:
 
(* An ordered list of the node names. *)
typedef nodenames_tnodenames (n : int) = list (String1, n)
 
(* A more efficient representation for nodes: integers in 0..n. *)
typedef nodenum_tnodenum (n : int) = [num : nat | num <= n - 1] size_t num
 
(* A collection of directed edges. *)
typedef edges_tedges (n : int) = arrayref (List0 (nodenum_tnodenum n), n)
 
(* An internal representation of data for a topological sort. *)
typedef toposort_ttopodata (n : int) =
'{
n = size_t n, (* The number of nodes. *)
edges = edges_tedges n, (* Directed edges. *)
tempmarks = marks_tmarks n, (* Temporary marks. *)
permmarks = marks_tmarks n (* Permanent marks. *)
}
 
fn
collect_nodenames
(desc : depdesc_tdepdesc)
:<!wrt> [n : nat]
@(nodenames_tnodenames n,
size_t n) =
let
Line 777:
.<m>.
(row : list (String1, m),
names : &nodenames_tnodenames n0 >> nodenames_tnodenames n1,
n : &size_t n0 >> size_t n1)
:<!wrt> #[n1 : int | n0 <= n1]
Line 802:
.<m>.
(desc : list (List1 String1, m),
names : &nodenames_tnodenames n0 >> nodenames_tnodenames n1,
n : &size_t n0 >> size_t n1)
:<!wrt> #[n1 : int | n0 <= n1]
Line 824:
nodename_number
{n : int}
(nodenames : nodenames_tnodenames n,
name : String1)
:<> Option (nodenum_tnodenum n) =
let
fun
loop {i : nat | i <= n}
.<n - i>.
(names : nodenames_tnodenames (n - i),
i : size_t i)
:<> Option (nodenum_tnodenum n) =
case+ names of
| NIL => None ()
Line 849:
fn
add_edge {n : int}
(edges : edges_tedges n,
from : nodenum_tnodenum n,
to : nodenum_tnodenum n)
:<!refwrt> void =
(* This implementation does not store duplicate edges. *)
let
val old_edges = edges[from]
implement list_find$pred<nodenum_tnodenum n> s = (s = to)
in
case+ list_find_opt<nodenum_tnodenum n> old_edges of
| ~ None_vt () => edges[from] := to :: old_edges
| ~ Some_vt _ => ()
Line 867:
{n : int}
{m : int}
(edges : edges_tedges n,
n : size_t n,
desc : depdesc_tdepdesc m,
nodenames : nodenames_tnodenames n)
:<!refwrt> void =
let
Line 893:
{m1 : nat}
.<m1>.
(headnum : nodenum_tnodenum n,
lst : list (String1, m1))
:<!refwrt> void =
Line 929:
 
fn
topodata_make
toposort_t_make
(desc : depdesc_tdepdesc)
:<!refwrt> [n : nat]
@(toposort_ttopodata n,
nodenames_tnodenames n) =
let
val @(nodenames, n) = collect_nodenames desc
Line 939:
prval [n : int] EQINT () = eqint_make_guint n
 
val edges = arrayref_make_elt<List0 (nodenum_tnodenum n)> (n, NIL)
val () = fill_edges {n} (edges, n, desc, nodenames)
 
val tempmarks = marks_t_make_eltmarks_make_elt (n, 0)
and permmarks = marks_t_make_eltmarks_make_elt (n, 0)
 
val topo =
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
find_unmarked_node
{n : int}
(topo : toposort_ttopodata n)
:<!ref> Option (nodenum_tnodenum n) =
let
val n = topo.n
Line 979 ⟶ 986:
.<n - i>.
(i : size_t i)
:<!ref> Option (nodenum_tnodenum n) =
if i = n then
None ()
Line 992 ⟶ 999:
fun
visit {n : int}
(topo : toposort_ttopodata n,
nodenum : nodenum_tnodenum n,
accum : List0 (nodenum_tnodenum n)),
:<!ntm,!refwrt> Option ( path : List0 (nodenum_tnodenum n)) =
: toporesult (nodenum n) =
(* Probably it is cumbersome to include a proof this routine
terminates. Thus I will not try to includewrite one. *)
let
val edgesn = topo.edgesn
and edges = topo.edges
and tempmarks = topo.tempmarks
and permmarks = topo.permmarks
in
if permmarks[nodenum] = 1 then
SomeTopo_SUCCESS accum
else if tempmarks[nodenum] = 1 then
None ()let
val () = assertloc (isneqz path)
in▼
Topo_CYCLE (list_vt2t (reverse path))
letend▼
else
let
Line 1,013 ⟶ 1,026:
{k : nat}
.<k>.
(topo : toposort_ttopodata n,
to_visit : list (nodenum_tnodenum n, k),
accum : List0 (nodenum_tnodenum n)),
:<!ntm,!refwrt> Option ( path : List0 (nodenum_tnodenum n)) =
: toporesult (nodenum n) =
case+ to_visit of
| NIL => SomeTopo_SUCCESS accum
| node_to_visit :: tail =>
begin
case+ visit (topo, node_to_visit, accum, path) of
| NoneTopo_SUCCESS ()accum1 => None ()
| Some accum1 => recursive_visits (topo, tail, accum1, path)
| other => other
end
in
tempmarks[nodenum] := 1;
case+ recursive_visits (topo, edges[nodenum], accum) of,
| None () => None ( nodenum :: path) of
| SomeTopo_SUCCESS accum1 =>
begin
tempmarks[nodenum] := 0;
permmarks[nodenum] := 1;
SomeTopo_SUCCESS (nodenum :: accum1)
end
| other => other
end
end
Line 1,041 ⟶ 1,057:
topological_sort
{n : int}
(topo : toposort_ttopodata n)
: toporesult (nodenum n, n) =
(* I do not bother to try to restrict effects. *)
: Option (list (nodenum_t n, n)) =
let
prval () = lemma_arrayref_param (topo.edges)
 
fun
sort (accum : List0 (nodenum_tnodenum n))
: Optiontoporesult (list (nodenum_tnodenum n, n)) =
case+ find_unmarked_node topo of
| None () =>
Line 1,056 ⟶ 1,071:
val () = assertloc (i2sz (length accum) = topo.n)
in
SomeTopo_SUCCESS accum
end
| Some nodenum =>
begin
case+ visit (topo, nodenum, accum, NIL) of
| NoneTopo_SUCCESS ()accum1 => Nonesort ()accum1
| SomeTopo_CYCLE accum1cycle => sortTopo_CYCLE accum1cycle
end
 
Line 1,081 ⟶ 1,096:
fn
find_a_valid_order
(desc : depdesc_tdepdesc)
: Option (List0toporesult String1) =▼
(* I do not bother to try to restrict effects. *)
▲ : Option (List0 String1) =
let
val @(topo, nodenames) = toposort_t_maketopodata_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
list_map$fopr<nodenum_tnodenum n><String1> i =
nodenames_array[i]
 
▲ in
macdef map = Some (list_vt2t (list_map<nodenum_tnodenum n><String1> valid_order))
endin
▲ case+ topological_sort topo of
▲ | SomeTopo_SUCCESS valid_order =>
Topo_SUCCESS (list_vt2t (map valid_order))
| Topo_CYCLE cycle =>
Topo_CYCLE (list_vt2t (map cycle))
end
 
Line 1,112 ⟶ 1,127:
in
case+ find_a_valid_order desc of
| Topo_SUCCESS valid_order =>
| None () => println! "**** dependency loop ****"
| Some valid_order => 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
 
Line 1,142 ⟶ 1,164:
ieee, dware, dw05, dw06, dw07, gtech, dw01, dw04, dw02, std_cell_lib, synopsys, std, dw03, ramlib, des_system_lib
</pre>
 
AND ...
 
Data fed to standard input:
<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>
 
Data from standard output:
<pre>
COMPILATION CYCLE: b, d, e, a, b
**** dependency loop ****
</pre>
 
''Note: I plan to enhance the function to return information about the cyclic dependency, rather than simply "None()".''
 
=={{header|Bracmat}}==
Chemoelectric
1,448

edits

Retrieved from "https://rosettacode.org/wiki/Special:MobileDiff/332305"