src/Provers/trancl.ML
changeset 32740 9dd0a2f83429
parent 32285 ab9b66c2bbca
child 32768 e4a3f9c3d4f5
equal deleted inserted replaced
32739:31e75ad9ae17 32740:9dd0a2f83429
   273 (*                                                                         *)
   273 (*                                                                         *)
   274 (* *********************************************************************** *)
   274 (* *********************************************************************** *)
   275 
   275 
   276 fun dfs eq_comp g u v =
   276 fun dfs eq_comp g u v =
   277  let
   277  let
   278     val pred = ref nil;
   278     val pred = Unsynchronized.ref [];
   279     val visited = ref nil;
   279     val visited = Unsynchronized.ref [];
   280 
   280 
   281     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   281     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   282 
   282 
   283     fun dfs_visit u' =
   283     fun dfs_visit u' =
   284     let val _ = visited := u' :: (!visited)
   284     let val _ = visited := u' :: (!visited)
   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  = ref nil;
   352   val visited  = Unsynchronized.ref nil;
   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