src/Provers/trancl.ML
 changeset 32768 e4a3f9c3d4f5 parent 32740 9dd0a2f83429 child 33063 4d462963a7db
equal inserted replaced
32767:2885e2a09f72 32768:e4a3f9c3d4f5
`   307 `
`   307 `
`   308 fun transpose eq_comp g =`
`   308 fun transpose eq_comp g =`
`   309   let`
`   309   let`
`   310    (* Compute list of reversed edges for each adjacency list *)`
`   310    (* Compute list of reversed edges for each adjacency list *)`
`   311    fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)`
`   311    fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)`
`   312      | flip (_,nil) = nil`
`   312      | flip (_,[]) = []`
`   313 `
`   313 `
`   314    (* Compute adjacency list for node u from the list of edges`
`   314    (* Compute adjacency list for node u from the list of edges`
`   315       and return a likewise reduced list of edges.  The list of edges`
`   315       and return a likewise reduced list of edges.  The list of edges`
`   316       is searches for edges starting from u, and these edges are removed. *)`
`   316       is searches for edges starting from u, and these edges are removed. *)`
`   317    fun gather (u,(v,w)::el) =`
`   317    fun gather (u,(v,w)::el) =`
`   319      val (adj,edges) = gather (u,el)`
`   319      val (adj,edges) = gather (u,el)`
`   320     in`
`   320     in`
`   321      if eq_comp (u, v) then (w::adj,edges)`
`   321      if eq_comp (u, v) then (w::adj,edges)`
`   322      else (adj,(v,w)::edges)`
`   322      else (adj,(v,w)::edges)`
`   323     end`
`   323     end`
`   324    | gather (_,nil) = (nil,nil)`
`   324    | gather (_,[]) = ([],[])`
`   325 `
`   325 `
`   326    (* For every node in the input graph, call gather to find all reachable`
`   326    (* For every node in the input graph, call gather to find all reachable`
`   327       nodes in the list of edges *)`
`   327       nodes in the list of edges *)`
`   328    fun assemble ((u,_)::el) edges =`
`   328    fun assemble ((u,_)::el) edges =`
`   329        let val (adj,edges) = gather (u,edges)`
`   329        let val (adj,edges) = gather (u,edges)`
`   330        in (u,adj) :: assemble el edges`
`   330        in (u,adj) :: assemble el edges`
`   331        end`
`   331        end`
`   332      | assemble nil _ = nil`
`   332      | assemble [] _ = []`
`   333 `
`   333 `
`   334    (* Compute, for each adjacency list, the list with reversed edges,`
`   334    (* Compute, for each adjacency list, the list with reversed edges,`
`   335       and concatenate these lists. *)`
`   335       and concatenate these lists. *)`
`   336    val flipped = List.foldr (op @) nil (map flip g)`
`   336    val flipped = maps flip g`
`   337 `
`   337 `
`   338  in assemble g flipped end`
`   338  in assemble g flipped end`
`   339 `
`   339 `
`   340 (* *********************************************************************** *)`
`   340 (* *********************************************************************** *)`
`   341 (*                                                                         *)`
`   341 (*                                                                         *)`
`   347 (* *********************************************************************** *)`
`   347 (* *********************************************************************** *)`
`   348 `
`   348 `
`   349 fun dfs_reachable eq_comp g u =`
`   349 fun dfs_reachable eq_comp g u =`
`   350  let`
`   350  let`
`   351   (* List of vertices which have been visited. *)`
`   351   (* List of vertices which have been visited. *)`
`   352   val visited  = Unsynchronized.ref nil;`
`   352   val visited  = Unsynchronized.ref [];`
`   353 `
`   353 `
`   354   fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)`
`   354   fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)`
`   355 `
`   355 `
`   356   fun dfs_visit g u  =`
`   356   fun dfs_visit g u  =`
`   357       let`
`   357       let`
`   358    val _ = visited := u :: !visited`
`   358    val _ = visited := u :: !visited`
`   359    val descendents =`
`   359    val descendents =`
`   360        List.foldr (fn ((v,l),ds) => if been_visited v then ds`
`   360        List.foldr (fn ((v,l),ds) => if been_visited v then ds`
`   361             else v :: dfs_visit g v @ ds)`
`   361             else v :: dfs_visit g v @ ds)`
`   362         nil (adjacent eq_comp g u)`
`   362         [] (adjacent eq_comp g u)`
`   363    in  descendents end`
`   363    in  descendents end`
`   364 `
`   364 `
`   365  in u :: dfs_visit g u end;`
`   365  in u :: dfs_visit g u end;`
`   366 `
`   366 `
`   367 (* *********************************************************************** *)`
`   367 (* *********************************************************************** *)`