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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
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 -> std_ppcmds
end
module Make = functor(S : SearchProblem) -> struct
type position = int list
let msg_with_position p pp =
let rec pp_rec = function
| [] -> mt ()
| [i] -> int i
| i :: l -> pp_rec l ++ str "." ++ int i
in
msg_debug (h 0 (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) = (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
|
