equal
deleted
inserted
replaced
637 end |
637 end |
638 | assemble nil _ = nil |
638 | assemble nil _ = nil |
639 |
639 |
640 (* Compute, for each adjacency list, the list with reversed edges, |
640 (* Compute, for each adjacency list, the list with reversed edges, |
641 and concatenate these lists. *) |
641 and concatenate these lists. *) |
642 val flipped = foldr (op @) nil (map flip g) |
642 val flipped = List.foldr (op @) nil (map flip g) |
643 |
643 |
644 in assemble g flipped end |
644 in assemble g flipped end |
645 |
645 |
646 (* *********************************************************************** *) |
646 (* *********************************************************************** *) |
647 (* *) |
647 (* *) |
675 (* Returns the nodes in the DFS tree rooted at u in g *) |
675 (* Returns the nodes in the DFS tree rooted at u in g *) |
676 fun dfs_visit g u : term list = |
676 fun dfs_visit g u : term list = |
677 let |
677 let |
678 val _ = visited := u :: !visited |
678 val _ = visited := u :: !visited |
679 val descendents = |
679 val descendents = |
680 foldr (fn ((v,l),ds) => if been_visited v then ds |
680 List.foldr (fn ((v,l),ds) => if been_visited v then ds |
681 else v :: dfs_visit g v @ ds) |
681 else v :: dfs_visit g v @ ds) |
682 nil (adjacent (op aconv) g u) |
682 nil (adjacent (op aconv) g u) |
683 in |
683 in |
684 finish := u :: !finish; |
684 finish := u :: !finish; |
685 descendents |
685 descendents |
725 |
725 |
726 fun dfs_visit g u : int list = |
726 fun dfs_visit g u : int list = |
727 let |
727 let |
728 val _ = visited := u :: !visited |
728 val _ = visited := u :: !visited |
729 val descendents = |
729 val descendents = |
730 foldr (fn ((v,l),ds) => if been_visited v then ds |
730 List.foldr (fn ((v,l),ds) => if been_visited v then ds |
731 else v :: dfs_visit g v @ ds) |
731 else v :: dfs_visit g v @ ds) |
732 nil (adjacent (op =) g u) |
732 nil (adjacent (op =) g u) |
733 in descendents end |
733 in descendents end |
734 |
734 |
735 in u :: dfs_visit g u end; |
735 in u :: dfs_visit g u end; |