Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: proof.mli Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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 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) : _ 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

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.