diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-05 14:11:40 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-05 14:11:40 +0000 |
commit | c034197e869cdc418b225b9abf25dee63a47e237 (patch) | |
tree | 42b5c9ecc4840c00ac1d31e5caf38b432953f7da /lib/explore.mli | |
parent | 9c88d6021a178cb64360bca75adbb6db030c480f (diff) |
module Explore générique et réécriture EAuto avec ce module; occur check dans clenv_merge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1425 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/explore.mli')
-rw-r--r-- | lib/explore.mli | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/lib/explore.mli b/lib/explore.mli new file mode 100644 index 000000000..5f484f8e6 --- /dev/null +++ b/lib/explore.mli @@ -0,0 +1,43 @@ + +(*i $Id$ i*) + +(*s Search strategies. *) + +(*s A search problem implements the following signature [SearchProblem]. + [state] is the type of states of the search tree. + [branching] is the branching function; if [branching s] returns an + empty list, then search from [s] is aborted; successors of [s] are + recursively searched in the order they appear in the list. + [success] determines whether a given state is a success. + + [pp] is a pretty-printer for states used in debugging versions of the + search functions. *) + +module type SearchProblem = sig + + type state + + val branching : state -> state list + + val success : state -> bool + + val pp : state -> unit + +end + +(*s Functor [Make] returns some search functions given a search problem. + Search functions raise [Not_found] if no success is found. + States are always visited in the order they appear in the + output of [branching] (whatever the search method is). + Debugging versions of the search functions print the position of the + visited state together with the state it-self (using [S.pp]). *) + +module Make : functor(S : SearchProblem) -> sig + + val depth_first : S.state -> S.state + val debug_depth_first : S.state -> S.state + + val breadth_first : S.state -> S.state + val debug_breadth_first : S.state -> S.state + +end |