author wenzelm Tue, 29 Sep 2009 23:19:26 +0200 changeset 32768 e4a3f9c3d4f5 parent 32767 2885e2a09f72 child 32769 511e6976f031
tuned;
 src/Provers/order.ML file | annotate | diff | comparison | revisions src/Provers/trancl.ML file | annotate | diff | comparison | revisions
```--- a/src/Provers/order.ML	Tue Sep 29 23:14:57 2009 +0200
+++ b/src/Provers/order.ML	Tue Sep 29 23:19:26 2009 +0200
@@ -611,7 +611,7 @@
let
(* Compute list of reversed edges for each adjacency list *)
fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
-     | flip (_,nil) = nil
+     | flip (_,[]) = []

(* Compute adjacency list for node u from the list of edges
and return a likewise reduced list of edges.  The list of edges
@@ -623,7 +623,7 @@
if eq_comp (u, v) then (w::adj,edges)
end
-   | gather (_,nil) = (nil,nil)
+   | gather (_,[]) = ([],[])

(* For every node in the input graph, call gather to find all reachable
nodes in the list of edges *)
@@ -631,11 +631,11 @@
let val (adj,edges) = gather (u,edges)
in (u,adj) :: assemble el edges
end
-     | assemble nil _ = nil
+     | assemble [] _ = []

(* Compute, for each adjacency list, the list with reversed edges,
and concatenate these lists. *)
-   val flipped = List.foldr (op @) nil (map flip g)
+   val flipped = maps flip g

in assemble g flipped end

@@ -675,7 +675,7 @@
val descendents =
List.foldr (fn ((v,l),ds) => if been_visited v then ds
else v :: dfs_visit g v @ ds)
-        nil (adjacent (op aconv) g u)
+        [] (adjacent (op aconv) g u)
in
finish := u :: !finish;
descendents
@@ -687,7 +687,7 @@
as yet unvisited. *)
app (fn u => if been_visited u then ()
else (dfs_visit G u; ()))  (members G);
-  visited := nil;
+  visited := [];

(* We don't reset finish because its value is used by
foldl below, and it will never be used again (even
@@ -699,7 +699,7 @@
list, which is what is returned. *)
Library.foldl (fn (comps,u) =>
if been_visited u then comps
-      else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps))  (nil,(!finish))
+      else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps))  ([],(!finish))
end;

@@ -725,7 +725,7 @@
val descendents =
List.foldr (fn ((v,l),ds) => if been_visited v then ds
else v :: dfs_visit g v @ ds)
-        nil (adjacent (op =) g u)
+        [] (adjacent (op =) g u)
in  descendents end

in u :: dfs_visit g u end;```
```--- a/src/Provers/trancl.ML	Tue Sep 29 23:14:57 2009 +0200
+++ b/src/Provers/trancl.ML	Tue Sep 29 23:19:26 2009 +0200
@@ -309,7 +309,7 @@
let
(* Compute list of reversed edges for each adjacency list *)
fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
-     | flip (_,nil) = nil
+     | flip (_,[]) = []

(* Compute adjacency list for node u from the list of edges
and return a likewise reduced list of edges.  The list of edges
@@ -321,7 +321,7 @@
if eq_comp (u, v) then (w::adj,edges)
end
-   | gather (_,nil) = (nil,nil)
+   | gather (_,[]) = ([],[])

(* For every node in the input graph, call gather to find all reachable
nodes in the list of edges *)
@@ -329,11 +329,11 @@
let val (adj,edges) = gather (u,edges)
in (u,adj) :: assemble el edges
end
-     | assemble nil _ = nil
+     | assemble [] _ = []

(* Compute, for each adjacency list, the list with reversed edges,
and concatenate these lists. *)
-   val flipped = List.foldr (op @) nil (map flip g)
+   val flipped = maps flip g

in assemble g flipped end

@@ -349,7 +349,7 @@
fun dfs_reachable eq_comp g u =
let
(* List of vertices which have been visited. *)
-  val visited  = Unsynchronized.ref nil;
+  val visited  = Unsynchronized.ref [];

fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)

@@ -359,7 +359,7 @@
val descendents =
List.foldr (fn ((v,l),ds) => if been_visited v then ds
else v :: dfs_visit g v @ ds)
-        nil (adjacent eq_comp g u)
+        [] (adjacent eq_comp g u)
in  descendents end

in u :: dfs_visit g u end;```