# HG changeset patch # User paulson # Date 826911548 -3600 # Node ID bc902840aab572d066ca394a8c9d6242a4fe6826 # Parent 97a305db0c9e8979227dd64998fa69f696ec6ef8 Search tacticals moved to search.ML diff -r 97a305db0c9e -r bc902840aab5 src/Pure/tctical.ML --- a/src/Pure/tctical.ML Fri Mar 15 18:38:24 1996 +0100 +++ b/src/Pure/tctical.ML Fri Mar 15 18:39:08 1996 +0100 @@ -6,7 +6,7 @@ Tacticals *) -infix 1 THEN THEN' THEN_BEST_FIRST; +infix 1 THEN THEN'; infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; infix 0 THEN_ELSE; @@ -19,13 +19,8 @@ val ALLGOALS : (int -> tactic) -> tactic val APPEND : tactic * tactic -> tactic val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic - val BREADTH_FIRST : (thm -> bool) -> tactic -> tactic val CHANGED : tactic -> tactic val COND : (thm -> bool) -> tactic -> tactic -> tactic - val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic - val DEPTH_SOLVE : tactic -> tactic - val DEPTH_SOLVE_1 : tactic -> tactic val DETERM : tactic -> tactic val EVERY : tactic list -> tactic val EVERY' : ('a -> tactic) list -> 'a -> tactic @@ -36,8 +31,6 @@ val FIRST1 : (int -> tactic) list -> tactic val FIRSTGOAL : (int -> tactic) -> tactic val goals_limit : int ref - val has_fewer_prems : int -> thm -> bool - val IF_UNSOLVED : tactic -> tactic val INTLEAVE : tactic * tactic -> tactic val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic val METAHYPS : (thm list -> tactic) -> int -> tactic @@ -63,13 +56,9 @@ val suppress_tracing : bool ref val THEN : tactic * tactic -> tactic val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic) - -> tactic val THEN_ELSE : tactic * (tactic*tactic) -> tactic val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic val tracify : bool ref -> tactic -> thm -> thm Sequence.seq - val trace_BEST_FIRST : bool ref - val trace_DEPTH_FIRST : bool ref val trace_REPEAT : bool ref val TRY : tactic -> tactic val TRYALL : (int -> tactic) -> tactic @@ -201,8 +190,6 @@ (*Tracing flags*) val trace_REPEAT= ref false -and trace_DEPTH_FIRST = ref false -and trace_BEST_FIRST = ref false and suppress_tracing = ref false; (*Handle all tracing commands for current state and tactic *) @@ -272,95 +259,6 @@ fun REPEAT1 tac = tac THEN REPEAT tac; -(** Search tacticals **) - -(*Searches until "satp" reports proof tree as satisfied. - Suppresses duplicate solutions to minimize search space.*) -fun DEPTH_FIRST satp tac = - let val tac = tracify trace_DEPTH_FIRST tac - fun depth used [] = None - | depth used (q::qs) = - case Sequence.pull q of - None => depth used qs - | Some(st,stq) => - if satp st andalso not (gen_mem eq_thm (st, used)) - then Some(st, Sequence.seqof - (fn()=> depth (st::used) (stq::qs))) - else depth used (tac st :: stq :: qs) - in traced_tac (fn st => depth [] ([Sequence.single st])) end; - - - -(*Predicate: Does the rule have fewer than n premises?*) -fun has_fewer_prems n rule = (nprems_of rule < n); - -(*Apply a tactic if subgoals remain, else do nothing.*) -val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; - -(*Tactical to reduce the number of premises by 1. - If no subgoals then it must fail! *) -fun DEPTH_SOLVE_1 tac = STATE - (fn st => - (case nprems_of st of - 0 => no_tac - | n => DEPTH_FIRST (has_fewer_prems n) tac)); - -(*Uses depth-first search to solve ALL subgoals*) -val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); - -(*** Best-first search ***) - -(*Insertion into priority queue of states *) -fun insert (nth: int*thm, []) = [nth] - | insert ((m,th), (n,th')::nths) = - if n some_of_list l)); - - -(* Best-first search for a state that satisfies satp (incl initial state) - Function sizef estimates size of problem remaining (smaller means better). - tactic tac0 sets up the initial priority queue, which is searched by tac. *) -fun tac0 THEN_BEST_FIRST (satp, sizef, tac1) = - let val tac = tracify trace_BEST_FIRST tac1 - fun pairsize th = (sizef th, th); - fun bfs (news,nprfs) = - (case partition satp news of - ([],nonsats) => next(foldr insert - (map pairsize nonsats, nprfs)) - | (sats,_) => some_of_list sats) - and next [] = None - | next ((n,prf)::nprfs) = - (if !trace_BEST_FIRST - then writeln("state size = " ^ string_of_int n ^ - " queue length =" ^ string_of_int (length nprfs)) - else (); - bfs (Sequence.list_of_s (tac prf), nprfs)) - fun btac st = bfs (Sequence.list_of_s (tac0 st), []) - in traced_tac btac end; - -(*Ordinary best-first search, with no initial tactic*) -fun BEST_FIRST (satp,sizef) tac = all_tac THEN_BEST_FIRST (satp,sizef,tac); - -(*Breadth-first search to satisfy satpred (including initial state) - SLOW -- SHOULD NOT USE APPEND!*) -fun BREADTH_FIRST satpred tac = - let val tacf = Sequence.list_of_s o tac; - fun bfs prfs = - (case partition satpred prfs of - ([],[]) => [] - | ([],nonsats) => - (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n"); - bfs (flat (map tacf nonsats))) - | (sats,_) => sats) - in (fn st => Sequence.s_of_list (bfs [st])) end; - - (** Filtering tacticals **) (*Returns all states satisfying the predicate*)