src/Pure/search.ML
changeset 4270 957c887b89b5
parent 3538 ed9de44032e0
child 5693 998af7667fa3
     1.1 --- a/src/Pure/search.ML	Fri Nov 21 15:26:22 1997 +0100
     1.2 +++ b/src/Pure/search.ML	Fri Nov 21 15:27:43 1997 +0100
     1.3 @@ -47,14 +47,14 @@
     1.4   let val tac = tracify trace_DEPTH_FIRST tac
     1.5       fun depth used [] = None
     1.6         | depth used (q::qs) =
     1.7 -	  case Sequence.pull q of
     1.8 +	  case Seq.pull q of
     1.9  	      None         => depth used qs
    1.10  	    | Some(st,stq) => 
    1.11  		if satp st andalso not (gen_mem eq_thm (st, used))
    1.12 -		then Some(st, Sequence.seqof
    1.13 +		then Some(st, Seq.make
    1.14  			         (fn()=> depth (st::used) (stq::qs)))
    1.15  		else depth used (tac st :: stq :: qs)
    1.16 -  in  traced_tac (fn st => depth [] ([Sequence.single st]))  end;
    1.17 +  in  traced_tac (fn st => depth [] ([Seq.single st]))  end;
    1.18  
    1.19  
    1.20  
    1.21 @@ -136,11 +136,11 @@
    1.22  		    writeln (string_of_int np ^ 
    1.23  			     implode (map (fn _ => "*") qs))
    1.24  		else ();
    1.25 -		Sequence.pull q) of
    1.26 +		Seq.pull q) of
    1.27  	     None         => depth (bnd,inc) qs
    1.28  	   | Some(st,stq) => 
    1.29  	       if satp st	(*solution!*)
    1.30 -	       then Some(st, Sequence.seqof
    1.31 +	       then Some(st, Seq.make
    1.32  			 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
    1.33  
    1.34  	       else 
    1.35 @@ -185,7 +185,7 @@
    1.36  
    1.37  (*For creating output sequence*)
    1.38  fun some_of_list []     = None
    1.39 -  | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
    1.40 +  | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
    1.41  
    1.42  
    1.43  (*Best-first search for a state that satisfies satp (incl initial state)
    1.44 @@ -205,8 +205,8 @@
    1.45  	       then writeln("state size = " ^ string_of_int n ^ 
    1.46  		         "  queue length =" ^ string_of_int (length nprfs))  
    1.47                 else ();
    1.48 -	     bfs (Sequence.list_of_s (tac prf), nprfs))
    1.49 -      fun btac st = bfs (Sequence.list_of_s (tac0 st),  [])
    1.50 +	     bfs (Seq.list_of (tac prf), nprfs))
    1.51 +      fun btac st = bfs (Seq.list_of (tac0 st),  [])
    1.52    in traced_tac btac end;
    1.53  
    1.54  (*Ordinary best-first search, with no initial tactic*)
    1.55 @@ -215,7 +215,7 @@
    1.56  (*Breadth-first search to satisfy satpred (including initial state) 
    1.57    SLOW -- SHOULD NOT USE APPEND!*)
    1.58  fun BREADTH_FIRST satpred tac = 
    1.59 -  let val tacf = Sequence.list_of_s o tac;
    1.60 +  let val tacf = Seq.list_of o tac;
    1.61        fun bfs prfs =
    1.62  	 (case  partition satpred prfs  of
    1.63  	      ([],[]) => []
    1.64 @@ -223,7 +223,7 @@
    1.65  		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
    1.66  		   bfs (List.concat (map tacf nonsats)))
    1.67  	    | (sats,_)  => sats)
    1.68 -  in (fn st => Sequence.s_of_list (bfs [st])) end;
    1.69 +  in (fn st => Seq.of_list (bfs [st])) end;
    1.70  
    1.71  
    1.72  (*  Author: 	Norbert Voelker, FernUniversitaet Hagen
    1.73 @@ -242,7 +242,7 @@
    1.74  
    1.75  (*For creating output sequence*)
    1.76  fun some_of_list []     = None
    1.77 -  | some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l));
    1.78 +  | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
    1.79  
    1.80  val trace_ASTAR = ref false; 
    1.81  
    1.82 @@ -262,8 +262,8 @@
    1.83  			 "  cost = " ^ string_of_int n ^ 
    1.84                           "  queue length =" ^ string_of_int (length nprfs))  
    1.85                 else ();
    1.86 -             bfs (Sequence.list_of_s (tf prf), nprfs,level+1))
    1.87 -      fun tf st = bfs (Sequence.list_of_s (tac0 st), [], 0)
    1.88 +             bfs (Seq.list_of (tf prf), nprfs,level+1))
    1.89 +      fun tf st = bfs (Seq.list_of (tac0 st), [], 0)
    1.90    in traced_tac tf end;
    1.91  
    1.92  (*Ordinary ASTAR, with no initial tactic*)