Topological sort: Difference between revisions
→{{header|Bracmat}}
(→Depth-first search: typo) |
|||
Line 494:
<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}}==
| |||