summaryrefslogtreecommitdiff
path: root/lib/explore.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/explore.ml')
-rw-r--r--lib/explore.ml22
1 files changed, 10 insertions, 12 deletions
diff --git a/lib/explore.ml b/lib/explore.ml
index c40362c8..1c8776a4 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <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 *)
(************************************************************************)
-(*i $Id: explore.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-open Format
+open Pp
(*s Definition of a search problem. *)
@@ -16,20 +14,20 @@ module type SearchProblem = sig
type state
val branching : state -> state list
val success : state -> bool
- val pp : state -> unit
+ val pp : state -> std_ppcmds
end
module Make = functor(S : SearchProblem) -> struct
type position = int list
- let pp_position p =
+ let msg_with_position p pp =
let rec pp_rec = function
- | [] -> ()
- | [i] -> printf "%d" i
- | i :: l -> pp_rec l; printf ".%d" i
+ | [] -> mt ()
+ | [i] -> int i
+ | i :: l -> pp_rec l ++ str "." ++ int i
in
- open_hbox (); pp_rec p; close_box ()
+ msg_debug (h 0 (pp_rec p) ++ pp)
(*s Depth first search. *)
@@ -42,7 +40,7 @@ module Make = functor(S : SearchProblem) -> struct
let debug_depth_first s =
let rec explore p s =
- pp_position p; S.pp 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
@@ -85,7 +83,7 @@ module Make = functor(S : SearchProblem) -> struct
explore q
| s :: l ->
let ps = i::p in
- pp_position ps; S.pp s;
+ 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]