Source file `explore.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp

(*s Definition of a search problem. *)

module type SearchProblem = sig
  type state
  val branching : state -> state list
  val success : state -> bool
  val pp : state -> Pp.t
end

module Make = functor(S : SearchProblem) -> struct

  type position = int list

  let msg_with_position (p : position) pp =
    let rec pp_rec = function
      | [] -> mt ()
      | [i] -> int i
      | i :: l -> pp_rec l ++ str "." ++ int i
    in
    Feedback.msg_debug (h (pp_rec p) ++ pp)

  (*s Depth first search. *)

  let rec depth_first s =
    if S.success s then s else depth_first_many (S.branching s)
  and depth_first_many = function
    | [] -> raise Not_found
    | [s] -> depth_first s
    | s :: l -> try depth_first s with Not_found -> depth_first_many l

  let debug_depth_first s =
    let rec explore p s =
      msg_with_position p (S.pp s);
      if S.success s then s else explore_many 1 p (S.branching s)
    and explore_many i p = function
      | [] -> raise Not_found
      | [s] -> explore (i::p) s
      | s :: l ->
          try explore (i::p) s with Not_found -> explore_many (succ i) p l
    in
    explore [1] s

  (*s Breadth first search. We use functional FIFOS à la Okasaki. *)

  type 'a queue = 'a list * 'a list

  exception Empty

  let empty = [],[]

  let push x (h,t) : _ queue = (x::h,t)

  let pop = function
    | h, x::t -> x, (h,t)
    | h, [] -> match List.rev h with x::t -> x, ([],t) | [] -> raise Empty

  let breadth_first s =
    let rec explore q =
      let (s, q') = try pop q with Empty -> raise Not_found in
      enqueue q' (S.branching s)
    and enqueue q = function
      | [] -> explore q
      | s :: l -> if S.success s then s else enqueue (push s q) l
    in
    enqueue empty [s]

  let debug_breadth_first s =
    let rec explore q =
      let ((p,s), q') = try pop q with Empty -> raise Not_found in
      enqueue 1 p q' (S.branching s)
    and enqueue i p q = function
      | [] ->
          explore q
      | s :: l ->
          let ps = i::p in
          msg_with_position ps (S.pp s);
          if S.success s then s else enqueue (succ i) p (push (ps,s) q) l
    in
    enqueue 1 [] empty [s]

end