Topological sort: Difference between revisions
Content added Content deleted
(→Depth-first search: typo) |
|||
Line 494: | Line 494: | ||
<pre>There is no topological sorting -- the Graph is cyclic!</pre> |
<pre>There is no topological sorting -- the Graph is cyclic!</pre> |
||
=={{header|ATS}}== |
|||
The program, for ATS2 (patsopt/patscc) and a garbage collector (Boehm GC). |
|||
<syntaxhighlight lang="ATS"> |
|||
(*------------------------------------------------------------------*) |
|||
(* The Rosetta Code topological sort task. *) |
|||
(*------------------------------------------------------------------*) |
|||
#include "share/atspre_staload.hats" |
|||
staload UN = "prelude/SATS/unsafe.sats" |
|||
#define NIL list_nil () |
|||
#define :: list_cons |
|||
(*------------------------------------------------------------------*) |
|||
local |
|||
(* A boolean type for setting marks, and a vector of those. *) |
|||
typedef _mark_t = [b : nat | b <= 1] uint8 b |
|||
typedef _marksvec_t (n : int) = arrayref (_mark_t, n) |
|||
implement g1int2uint<intknd, uint8knd> i = $UN.cast i |
|||
implement g1uint2int<uint8knd, intknd> i = $UN.cast i |
|||
in |
|||
abstype marks_t (n : int) |
|||
assume marks_t n = _marksvec_t n |
|||
fn marks_t_make_elt |
|||
{n : nat} |
|||
{b : int | b == 0 || b == 1} |
|||
(n : size_t n, |
|||
b : int b) |
|||
:<!wrt> _marksvec_t n = |
|||
arrayref_make_elt (n, g1i2u b) |
|||
fn |
|||
marks_t_set_at |
|||
{n : int} |
|||
{i : nat | i < n} |
|||
{b : int | b == 0 || b == 1} |
|||
(vec : _marksvec_t n, |
|||
i : size_t i, |
|||
b : int b) |
|||
:<!refwrt> void = |
|||
vec[i] := g1i2u b |
|||
fn |
|||
marks_t_get_at |
|||
{n : int} |
|||
{i : nat | i < n} |
|||
(vec : _marksvec_t n, |
|||
i : size_t i) |
|||
:<!ref> [b : int | b == 0 || b == 1] |
|||
int b = |
|||
g1u2i vec[i] |
|||
fn |
|||
marks_t_setall |
|||
{n : int} |
|||
{b : int | b == 0 || b == 1} |
|||
(vec : _marksvec_t n, |
|||
n : size_t n, |
|||
b : int b) |
|||
:<!refwrt> void = |
|||
let |
|||
prval () = lemma_arrayref_param vec |
|||
var i : [i : nat | i <= n] size_t i |
|||
in |
|||
for* {i : nat | i <= n} |
|||
.<n - i>. |
|||
(i : size_t i) => |
|||
(i := i2sz 0; i <> n; i := succ i) |
|||
vec[i] := g1i2u b |
|||
end |
|||
overload [] with marks_t_set_at of 100 |
|||
overload [] with marks_t_get_at of 100 |
|||
overload setall with marks_t_setall of 100 |
|||
end |
|||
(*------------------------------------------------------------------*) |
|||
(* Reading dependencies from a file. The format is kept very simple, |
|||
because this is not a task about parsing. (Though I have written |
|||
an S-expression parser in ATS, and there is JSON support in the |
|||
ATS contributions package.) *) |
|||
(* The format of a dependencies description. The second and later |
|||
entries of each sublist forms the list of dependencies of the first |
|||
entry. Thus this is a kind of association list. *) |
|||
typedef depdesc_t (n : int) = list (List1 String1, n) |
|||
typedef depdesc_t = [n : nat] depdesc_t n |
|||
typedef char_skipper_t = |
|||
{n : int} |
|||
{i : nat | i <= n} |
|||
(string n, |
|||
size_t n, |
|||
size_t i) -<cloref> (* A closure. *) |
|||
[j : int | i <= j; j <= n] |
|||
size_t j |
|||
fn |
|||
make_char_skipper |
|||
(match : char -<> bool) |
|||
:<> char_skipper_t = |
|||
let |
|||
fun |
|||
skipper {n : int} |
|||
{i : nat | i <= n} |
|||
.<n - i>. |
|||
(s : string n, |
|||
n : size_t n, |
|||
i : size_t i) |
|||
:<cloref> [j : int | i <= j; j <= n] |
|||
size_t j = |
|||
if i = n then |
|||
i |
|||
else if ~match s[i] then |
|||
i |
|||
else |
|||
skipper (s, n, succ i) |
|||
in |
|||
skipper (* Return a closure. *) |
|||
end |
|||
val skip_spaces = make_char_skipper (lam c => isspace c) |
|||
val skip_ident = |
|||
make_char_skipper (lam c => (~isspace c) * (c <> ';')) |
|||
fn is_end_of_list (c : char) :<> bool = (c = ';') |
|||
fn |
|||
read_row {n : int} |
|||
{i : nat | i <= n} |
|||
(text : string n, |
|||
n : size_t n, |
|||
i : size_t i) |
|||
:<!wrt> [j : int | i <= j; j <= n] |
|||
@(List0 String1, size_t j) = |
|||
let |
|||
fun |
|||
loop {i : nat | i <= n} |
|||
.<n - i>. |
|||
(row : List0 String1, |
|||
i : size_t i) |
|||
:<!wrt> [j : int | i <= j; j <= n] |
|||
@(List0 String1, size_t j) = |
|||
let |
|||
val i = skip_spaces (text, n, i) |
|||
in |
|||
if i = n then |
|||
@(list_vt2t (reverse row), i) |
|||
else if is_end_of_list text[i] then |
|||
@(list_vt2t (reverse row), succ i) |
|||
else |
|||
let |
|||
val j = skip_ident (text, n, i) |
|||
val () = $effmask_exn assertloc (i < j) |
|||
val nodename = |
|||
strnptr2string |
|||
(string_make_substring (text, i, j - i)) |
|||
in |
|||
loop (nodename :: row, j) |
|||
end |
|||
end |
|||
in |
|||
loop (NIL, i) |
|||
end |
|||
fn |
|||
read_desc {n : int} |
|||
{i : nat | i <= n} |
|||
(text : string n, |
|||
n : size_t n, |
|||
i : size_t i) |
|||
:<!wrt> [j : int | i <= j; j <= n] |
|||
@(depdesc_t, size_t j) = |
|||
let |
|||
fun |
|||
loop {i : nat | i <= n} |
|||
.<n - i>. |
|||
(desc : depdesc_t, |
|||
i : size_t i) |
|||
:<!wrt> [j : int | i <= j; j <= n] |
|||
@(depdesc_t, size_t j) = |
|||
let |
|||
val i = skip_spaces (text, n, i) |
|||
in |
|||
if i = n then |
|||
@(list_vt2t (reverse desc), i) |
|||
else if is_end_of_list text[i] then |
|||
@(list_vt2t (reverse desc), succ i) |
|||
else |
|||
let |
|||
val @(row, j) = read_row (text, n, i) |
|||
val () = $effmask_exn assertloc (i < j) |
|||
in |
|||
if length row = 0 then |
|||
loop (desc, j) |
|||
else |
|||
loop (row :: desc, j) |
|||
end |
|||
end |
|||
in |
|||
loop (NIL, i) |
|||
end |
|||
fn |
|||
read_to_string () |
|||
: String = |
|||
(* This simple implementation reads input only up to a certain |
|||
size. *) |
|||
let |
|||
#define BUFSIZE 8296 |
|||
var buf = @[char][BUFSIZE] ('\0') |
|||
var c : int = $extfcall (int, "getchar") |
|||
var i : Size_t = i2sz 0 |
|||
in |
|||
while ((0 <= c) * (i < pred (i2sz BUFSIZE))) |
|||
begin |
|||
buf[i] := int2char0 c; |
|||
i := succ i; |
|||
c := $extfcall (int, "getchar") |
|||
end; |
|||
strptr2string (string0_copy ($UN.cast{string} (addr@ buf))) |
|||
end |
|||
fn |
|||
read_depdesc () |
|||
: depdesc_t = |
|||
let |
|||
val text = read_to_string () |
|||
prval () = lemma_string_param text |
|||
val n = strlen text |
|||
val @(desc, _) = read_desc (text, n, i2sz 0) |
|||
in |
|||
desc |
|||
end |
|||
(*------------------------------------------------------------------*) |
|||
(* Conversion of a dependencies description to the internal |
|||
representation for a topological sort. *) |
|||
(* An ordered list of the node names. *) |
|||
typedef nodenames_t (n : int) = list (String1, n) |
|||
(* A more efficient representation for nodes: integers in 0..n. *) |
|||
typedef nodenum_t (n : int) = [num : nat | num <= n - 1] size_t num |
|||
(* A collection of directed edges. *) |
|||
typedef edges_t (n : int) = arrayref (List0 (nodenum_t n), n) |
|||
(* An internal representation of data for a topological sort. *) |
|||
typedef toposort_t (n : int) = |
|||
'{ |
|||
n = size_t n, (* The number of nodes. *) |
|||
edges = edges_t n, (* Directed edges. *) |
|||
tempmarks = marks_t n, (* Temporary marks. *) |
|||
permmarks = marks_t n (* Permanent marks. *) |
|||
} |
|||
fn |
|||
collect_nodenames |
|||
(desc : depdesc_t) |
|||
:<!wrt> [n : nat] |
|||
@(nodenames_t n, |
|||
size_t n) = |
|||
let |
|||
fun |
|||
collect_row |
|||
{m : nat} |
|||
{n0 : nat} |
|||
.<m>. |
|||
(row : list (String1, m), |
|||
names : &nodenames_t n0 >> nodenames_t n1, |
|||
n : &size_t n0 >> size_t n1) |
|||
:<!wrt> #[n1 : int | n0 <= n1] |
|||
void = |
|||
case+ row of |
|||
| NIL => () |
|||
| head :: tail => |
|||
let |
|||
implement list_find$pred<String1> s = (s = head) |
|||
in |
|||
case+ list_find_opt<String1> names of |
|||
| ~ None_vt () => |
|||
begin |
|||
names := head :: names; |
|||
n := succ n; |
|||
collect_row (tail, names, n) |
|||
end |
|||
| ~ Some_vt _ => collect_row (tail, names, n) |
|||
end |
|||
fun |
|||
collect {m : nat} |
|||
{n0 : nat} |
|||
.<m>. |
|||
(desc : list (List1 String1, m), |
|||
names : &nodenames_t n0 >> nodenames_t n1, |
|||
n : &size_t n0 >> size_t n1) |
|||
:<!wrt> #[n1 : int | n0 <= n1] |
|||
void = |
|||
case+ desc of |
|||
| NIL => () |
|||
| head :: tail => |
|||
begin |
|||
collect_row (head, names, n); |
|||
collect (tail, names, n) |
|||
end |
|||
var names : List0 String1 = NIL |
|||
var n : Size_t = i2sz 0 |
|||
in |
|||
collect (desc, names, n); |
|||
@(list_vt2t (reverse names), n) |
|||
end |
|||
fn |
|||
nodename_number |
|||
{n : int} |
|||
(nodenames : nodenames_t n, |
|||
name : String1) |
|||
:<> Option (nodenum_t n) = |
|||
let |
|||
fun |
|||
loop {i : nat | i <= n} |
|||
.<n - i>. |
|||
(names : nodenames_t (n - i), |
|||
i : size_t i) |
|||
:<> Option (nodenum_t n) = |
|||
case+ names of |
|||
| NIL => None () |
|||
| head :: tail => |
|||
if head = name then |
|||
Some i |
|||
else |
|||
loop (tail, succ i) |
|||
prval () = lemma_list_param nodenames |
|||
in |
|||
loop (nodenames, i2sz 0) |
|||
end |
|||
fn |
|||
add_edge {n : int} |
|||
(edges : edges_t n, |
|||
from : nodenum_t n, |
|||
to : nodenum_t n) |
|||
:<!refwrt> void = |
|||
(* This implementation does not store duplicate edges. *) |
|||
let |
|||
val old_edges = edges[from] |
|||
implement list_find$pred<nodenum_t n> s = (s = to) |
|||
in |
|||
case+ list_find_opt<nodenum_t n> old_edges of |
|||
| ~ None_vt () => edges[from] := to :: old_edges |
|||
| ~ Some_vt _ => () |
|||
end |
|||
fn |
|||
fill_edges |
|||
{n : int} |
|||
{m : int} |
|||
(edges : edges_t n, |
|||
n : size_t n, |
|||
desc : depdesc_t m, |
|||
nodenames : nodenames_t n) |
|||
:<!refwrt> void = |
|||
let |
|||
prval () = lemma_list_param desc |
|||
prval () = lemma_list_param nodenames |
|||
fn |
|||
clear_edges () |
|||
:<!refwrt> void = |
|||
let |
|||
var i : [i : nat | i <= n] size_t i |
|||
in |
|||
for* {i : nat | i <= n} |
|||
.<n - i>. |
|||
(i : size_t i) => |
|||
(i := i2sz 0; i <> n; i := succ i) |
|||
edges[i] := NIL |
|||
end |
|||
fun |
|||
fill_from_desc_entry |
|||
{m1 : nat} |
|||
.<m1>. |
|||
(headnum : nodenum_t n, |
|||
lst : list (String1, m1)) |
|||
:<!refwrt> void = |
|||
case+ lst of |
|||
| NIL => () |
|||
| name :: tail => |
|||
let |
|||
val- Some num = nodename_number (nodenames, name) |
|||
in |
|||
if num <> headnum then |
|||
add_edge {n} (edges, num, headnum); |
|||
fill_from_desc_entry (headnum, tail) |
|||
end |
|||
fun |
|||
fill_from_desc |
|||
{m2 : nat} |
|||
.<m2>. |
|||
(lst : list (List1 String1, m2)) |
|||
:<!refwrt> void = |
|||
case+ lst of |
|||
| NIL => () |
|||
| list_entry :: tail => |
|||
let |
|||
val+ headname :: desc_entry = list_entry |
|||
val- Some headnum = nodename_number (nodenames, headname) |
|||
in |
|||
fill_from_desc_entry (headnum, desc_entry); |
|||
fill_from_desc tail |
|||
end |
|||
in |
|||
clear_edges (); |
|||
fill_from_desc desc |
|||
end |
|||
fn |
|||
toposort_t_make |
|||
(desc : depdesc_t) |
|||
:<!refwrt> [n : nat] |
|||
@(toposort_t n, |
|||
nodenames_t n) = |
|||
let |
|||
val @(nodenames, n) = collect_nodenames desc |
|||
prval () = lemma_g1uint_param n |
|||
prval [n : int] EQINT () = eqint_make_guint n |
|||
val edges = arrayref_make_elt<List0 (nodenum_t n)> (n, NIL) |
|||
val () = fill_edges {n} (edges, n, desc, nodenames) |
|||
val tempmarks = marks_t_make_elt (n, 0) |
|||
and permmarks = marks_t_make_elt (n, 0) |
|||
val topo = |
|||
'{ |
|||
n = n, |
|||
edges = edges, |
|||
tempmarks = tempmarks, |
|||
permmarks = permmarks |
|||
} |
|||
in |
|||
@(topo, nodenames) |
|||
end |
|||
(*------------------------------------------------------------------*) |
|||
(* |
|||
Topological sort by depth-first search. See |
|||
https://en.wikipedia.org/w/index.php?title=Topological_sorting&oldid=1092588874#Depth-first_search |
|||
*) |
|||
fn |
|||
find_unmarked_node |
|||
{n : int} |
|||
(topo : toposort_t n) |
|||
:<!ref> Option (nodenum_t n) = |
|||
let |
|||
val n = topo.n |
|||
and permmarks = topo.permmarks |
|||
prval () = lemma_g1uint_param n |
|||
fun |
|||
loop {i : nat | i <= n} |
|||
.<n - i>. |
|||
(i : size_t i) |
|||
:<!ref> Option (nodenum_t n) = |
|||
if i = n then |
|||
None () |
|||
else if permmarks[i] = 0 then |
|||
Some i |
|||
else |
|||
loop (succ i) |
|||
in |
|||
loop (i2sz 0) |
|||
end |
|||
fun |
|||
visit {n : int} |
|||
(topo : toposort_t n, |
|||
nodenum : nodenum_t n, |
|||
accum : List0 (nodenum_t n)) |
|||
:<!ntm,!refwrt> Option (List0 (nodenum_t n)) = |
|||
(* Probably it is cumbersome to include a proof this routine |
|||
terminates. Thus I will not try to include one. *) |
|||
let |
|||
val edges = topo.edges |
|||
and tempmarks = topo.tempmarks |
|||
and permmarks = topo.permmarks |
|||
in |
|||
if permmarks[nodenum] = 1 then |
|||
Some accum |
|||
else if tempmarks[nodenum] = 1 then |
|||
None () |
|||
else |
|||
let |
|||
fun |
|||
recursive_visits |
|||
{k : nat} |
|||
.<k>. |
|||
(topo : toposort_t n, |
|||
to_visit : list (nodenum_t n, k), |
|||
accum : List0 (nodenum_t n)) |
|||
:<!ntm,!refwrt> Option (List0 (nodenum_t n)) = |
|||
case+ to_visit of |
|||
| NIL => Some accum |
|||
| node_to_visit :: tail => |
|||
begin |
|||
case+ visit (topo, node_to_visit, accum) of |
|||
| None () => None () |
|||
| Some accum1 => recursive_visits (topo, tail, accum1) |
|||
end |
|||
in |
|||
tempmarks[nodenum] := 1; |
|||
case+ recursive_visits (topo, edges[nodenum], accum) of |
|||
| None () => None () |
|||
| Some accum1 => |
|||
begin |
|||
tempmarks[nodenum] := 0; |
|||
permmarks[nodenum] := 1; |
|||
Some (nodenum :: accum1) |
|||
end |
|||
end |
|||
end |
|||
fn |
|||
topological_sort |
|||
{n : int} |
|||
(topo : toposort_t 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_t n)) |
|||
: Option (list (nodenum_t n, n)) = |
|||
case+ find_unmarked_node topo of |
|||
| None () => |
|||
let |
|||
prval () = lemma_list_param accum |
|||
val () = assertloc (i2sz (length accum) = topo.n) |
|||
in |
|||
Some accum |
|||
end |
|||
| Some nodenum => |
|||
begin |
|||
case+ visit (topo, nodenum, accum) of |
|||
| None () => None () |
|||
| Some accum1 => sort accum1 |
|||
end |
|||
val () = setall (topo.tempmarks, topo.n, 0) |
|||
and () = setall (topo.permmarks, topo.n, 0) |
|||
val accum = sort NIL |
|||
val () = setall (topo.tempmarks, topo.n, 0) |
|||
and () = setall (topo.permmarks, topo.n, 0) |
|||
in |
|||
accum |
|||
end |
|||
(*------------------------------------------------------------------*) |
|||
(* The function asked for in the task. *) |
|||
fn |
|||
find_a_valid_order |
|||
(desc : depdesc_t) |
|||
(* I do not bother to try to restrict effects. *) |
|||
: Option (List0 String1) = |
|||
let |
|||
val @(topo, nodenames) = toposort_t_make desc |
|||
in |
|||
case+ topological_sort topo of |
|||
| None () => None () |
|||
| Some valid_order => |
|||
let |
|||
val nodenames_array = |
|||
arrayref_make_list<String1> (sz2i (topo.n), nodenames) |
|||
prval [n : int] EQINT () = eqint_make_guint (topo.n) |
|||
implement |
|||
list_map$fopr<nodenum_t n><String1> i = |
|||
nodenames_array[i] |
|||
in |
|||
Some (list_vt2t (list_map<nodenum_t n><String1> valid_order)) |
|||
end |
|||
end |
|||
(*------------------------------------------------------------------*) |
|||
implement |
|||
main0 (argc, argv) = |
|||
let |
|||
val desc = read_depdesc () |
|||
in |
|||
case+ find_a_valid_order desc of |
|||
| None () => println! "**** dependency loop ****" |
|||
| Some valid_order => println! (valid_order : List0 string) |
|||
end |
|||
(*------------------------------------------------------------------*) |
|||
</syntaxhighlight> |
|||
=={{header|Bracmat}}== |
=={{header|Bracmat}}== |