(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) Jean-Christophe Filliatre                               *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(*s Functional search *)

module type FunctionalProblem = sig
  type state
  type move
  val success : state -> bool
  val moves : state -> (move * state) list
  type table
  val create : unit -> table
  val add : table -> state -> unit
  val mem : table -> state -> bool
  val clear : table -> unit
end

(* Depth-first search *)
module FunctionalDFS(P : FunctionalProblem) = struct

  let search s0 =
    let visited = P.create () in
    let already s = (P.mem visited s) || (P.add visited s; false) in
    let rec dfs path s =
      if already s then raise Not_found;
      if P.success s then s, List.rev path else first path (P.moves s)
    and first path = function
      | [] -> raise Not_found
      | (m,s) :: r -> try dfs (m :: path) s with Not_found -> first path r
    in
    dfs [] s0

  let search s0 =
    let visited = P.create () in
    let already s = (P.mem visited s) || (P.add visited s; false) in
    let rec dfs = function
      | [] ->
          raise Not_found
      | (path,s) :: _ when P.success s ->
          s, List.rev path
      | (path,s) :: stack ->
          dfs
            (List.fold_left
               (fun stack (m,s') ->
                  if already s' then stack else (m :: path, s') :: stack)
               stack (P.moves s))
    in
    let _ = already s0 in
    dfs [[], s0]

end

(* Breadth-first search *)
module FunctionalBFS(P : FunctionalProblem) = struct

  let search s0 =
    let visited = P.create () in
    (* meaning is here ``already queued'' *)
    let already s = (P.mem visited s) || (P.add visited s; false) in
    let _ = already s0 in
    let q = Queue.create () in
    Queue.add ([],s0) q;
    let rec bfs () =
      if Queue.length q = 0 then raise Not_found;
      let path,s = Queue.take q in
      if P.success s then
        s, List.rev path
      else begin
        List.iter
          (fun (m,s') -> if not (already s') then Queue.add (m :: path, s') q)
          (P.moves s);
        bfs ()
      end
    in
    bfs ()

  (* variant without Queue: we use two lists instead and we don't even care
     about reversing the second one when the first becomes empty, since order
     within a given level is unimportant *)
  (*i
  let search s0 =
    let visited = Hashtbl.create 65537 in
    (* meaning is here ``already queued'' *)
    let already s = match P.mark s with
      | None -> false
      | Some h -> (Hashtbl.mem visited h) || (Hashtbl.add visited h (); false)
    in
    let _ = already s0 in
    let rec bfs nextl = function
      | [] ->
          if nextl = [] then raise Not_found; bfs [] nextl
      | (path,s) :: r ->
          if P.success s then
            s, List.rev path
          else
            bfs
              (List.fold_left
                  (fun n (m,s') -> if already s' then n else (m::path,s') :: n)
                  nextl (P.moves s)) r
    in
    bfs [] [[],s0]
    i*)
end

(* Iterative deepening search *)
module FunctionalIDS(P : FunctionalProblem) = struct

  let search s0 =
    let visited = P.create () in
    let already s = (P.mem visited s) || (P.add visited s; false) in
    let depth max =
      let rec dfs n path s =
        if n > max || already s then raise Not_found;
        if P.success s then s, List.rev path else first n path (P.moves s)
      and first n path = function
        | [] ->
            raise Not_found
        | (m,s) :: r ->
            try dfs (succ n) (m :: path) s with Not_found -> first n path r
      in
      dfs 0 [] s0
    in
    let rec try_depth d =
      try depth d with Not_found -> P.clear visited; try_depth (succ d)
    in
    try_depth 0

end


(*s Imperative search *)

module type ImperativeProblem = sig
  type move
  val success : unit -> bool
  val moves : unit -> move list
  val do_move : move -> unit
  val undo_move : move -> unit
  val add : unit -> unit
  val mem : unit -> bool
  val clear : unit -> unit
end

(* Depth-first search *)
module ImperativeDFS(P : ImperativeProblem) = struct

  let iter f =
    let already () = (P.mem ()) || (P.add (); false) in
    let rec dfs path =
      if not (already ()) then
        if P.success () then f (List.rev path) else first path (P.moves ())
    and first path = function
      | [] ->
          ()
      | m :: r ->
          P.do_move m; dfs (m :: path); P.undo_move m; first path r
    in
    dfs []

  let search () =
    let already () = (P.mem ()) || (P.add (); false) in
    let rec dfs path =
      if already () then raise Not_found;
      if P.success () then List.rev path else first path (P.moves ())
    and first path = function
      | [] ->
          raise Not_found
      | m :: r ->
          try P.do_move m; dfs (m :: path)
          with Not_found -> P.undo_move m; first path r
    in
    dfs []

end

(* Breadth-first search *)
module ImperativeBFS(P : ImperativeProblem) = struct

  (* cut [n] elements at head of list [l] *)
  let rec cut_head n l = if n == 0 then l else cut_head (pred n) (List.tl l)

  (* find the common physical suffix of [l1] and [l2] *)
  let common_psuffix (n1,l1) (n2,l2) =
    (* [suffix] applies when the two lists have same length *)
    let rec suffix l1 l2 =
      if l1 == l2 then l1 else suffix (List.tl l1) (List.tl l2)
    in
    if n1 < n2 then suffix l1 (cut_head (n2 - n1) l2)
    else if n2 < n1 then suffix (cut_head (n1 - n2) l1) l2
    else suffix l1 l2

  let search () =
    let already () = (P.mem ()) || (P.add (); false) in
    let q = Queue.create () in
    Queue.add (0,[]) q;
    let cpath = ref (0,[]) in
    let rec restore_state path =
      let suf = common_psuffix path !cpath in
      let rec backward = function
        | (m :: r) as p when p != suf -> P.undo_move m; backward r
        | _ -> ()
      in
      let rec forward = function
        | (m :: r) as p when p != suf -> forward r; P.do_move m
        | _ -> ()
      in
      backward (snd !cpath);
      forward (snd path);
      cpath := path
    in
    let rec bfs () =
      if Queue.length q = 0 then raise Not_found;
      let (n,path) as s = Queue.take q in
      restore_state s;
      if P.success () then
        List.rev path
      else if not (already ()) then begin
        List.iter (fun m -> Queue.add (succ n, m :: path) q) (P.moves ());
        bfs ()
      end else
        bfs ()
    in
    bfs ()

end

(* Iterative deepening search *)
module ImperativeIDS(P : ImperativeProblem) = struct

  let search () =
    let already () = (P.mem ()) || (P.add (); false) in
    let depth max =
      let rec dfs n path =
        if n > max || already () then raise Not_found;
        if P.success () then List.rev path else first n path (P.moves ())
      and first n path = function
        | [] ->
            raise Not_found
        | m :: r ->
            try P.do_move m; dfs (succ n) (m :: path)
            with Not_found -> P.undo_move m; first n path r
      in
      dfs 0 []
    in
    let rec try_depth d =
      Printf.eprintf "trying depth %d...\n" d; flush stderr;
      try depth d with Not_found -> P.clear (); try_depth (succ d)
    in
    try_depth 0

end

This document was generated using caml2html