# HG changeset patch # User wenzelm # Date 1439671623 -7200 # Node ID 4c108cce6b3565e21a81c3c90bc7f631a5b3756e # Parent dc5b7982e324bb9c2f51e2d3cd740900834c6592 tuned whitespace; diff -r dc5b7982e324 -r 4c108cce6b35 src/Pure/search.ML --- a/src/Pure/search.ML Sat Aug 15 20:27:23 2015 +0200 +++ b/src/Pure/search.ML Sat Aug 15 22:47:03 2015 +0200 @@ -1,5 +1,6 @@ (* Title: Pure/search.ML - Author: Lawrence C Paulson and Norbert Voelker + Author: Lawrence C Paulson + Author: Norbert Voelker, FernUniversitaet Hagen Search tacticals. *) @@ -41,18 +42,17 @@ (*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 Seq.pull q of - NONE => depth used qs - | SOME(st,stq) => - if satp st andalso not (member Thm.eq_thm used st) - then SOME(st, Seq.make - (fn()=> depth (st::used) (stq::qs))) - else depth used (tac st :: stq :: qs) - in traced_tac (fn st => depth [] [Seq.single st]) end; - + let + val tac = tracify trace_DEPTH_FIRST tac + fun depth used [] = NONE + | depth used (q :: qs) = + (case Seq.pull q of + NONE => depth used qs + | SOME (st, stq) => + if satp st andalso not (member Thm.eq_thm used st) then + SOME (st, Seq.make (fn() => depth (st :: used) (stq :: qs))) + else depth used (tac st :: stq :: qs)); + in traced_tac (fn st => depth [] [Seq.single st]) end; (*Predicate: Does the rule have fewer than n premises?*) @@ -86,8 +86,8 @@ (**** Iterative deepening with pruning ****) fun has_vars (Var _) = true - | has_vars (Abs (_,_,t)) = has_vars t - | has_vars (f$t) = has_vars f orelse has_vars t + | has_vars (Abs (_, _, t)) = has_vars t + | has_vars (f $ t) = has_vars f orelse has_vars t | has_vars _ = false; (*Counting of primitive inferences is APPROXIMATE, as the step tactic @@ -95,21 +95,21 @@ (*Pruning of rigid ancestor to prevent backtracking*) fun prune (new as (k', np':int, rgd', stq), qs) = - let fun prune_aux (qs, []) = new::qs - | prune_aux (qs, (k,np,rgd,q)::rqs) = - if np'+1 = np andalso rgd then - (if !trace_DEPTH_FIRST then - tracing ("Pruning " ^ - string_of_int (1+length rqs) ^ " levels") - else (); - (*Use OLD k: zero-cost solution; see Stickel, p 365*) - (k, np', rgd', stq) :: qs) - else prune_aux ((k,np,rgd,q)::qs, rqs) - fun take ([], rqs) = ([], rqs) - | take (arg as ((k,np,rgd,stq)::qs, rqs)) = - if np' < np then take (qs, (k,np,rgd,stq)::rqs) - else arg - in prune_aux (take (qs, [])) end; + let + fun prune_aux (qs, []) = new :: qs + | prune_aux (qs, (k, np, rgd, q) :: rqs) = + if np' + 1 = np andalso rgd then + (if !trace_DEPTH_FIRST then + tracing ("Pruning " ^ + string_of_int (1+length rqs) ^ " levels") + else (); + (*Use OLD k: zero-cost solution; see Stickel, p 365*) + (k, np', rgd', stq) :: qs) + else prune_aux ((k, np, rgd, q) :: qs, rqs) + fun take ([], rqs) = ([], rqs) + | take (arg as ((k, np, rgd, stq) :: qs, rqs)) = + if np' < np then take (qs, (k, np, rgd, stq) :: rqs) else arg; + in prune_aux (take (qs, [])) end; (*Depth-first iterative deepening search for a state that satisfies satp @@ -118,54 +118,51 @@ to suppress solutions arising from earlier searches, as the accumulated cost (k) can be wrong.*) fun THEN_ITER_DEEPEN lim tac0 satp tac1 = traced_tac (fn st => - let val countr = Unsynchronized.ref 0 - and tf = tracify trace_DEPTH_FIRST (tac1 1) - and qs0 = tac0 st + let + val countr = Unsynchronized.ref 0 + and tf = tracify trace_DEPTH_FIRST (tac1 1) + and qs0 = tac0 st (*bnd = depth bound; inc = estimate of increment required next*) - fun depth (bnd,inc) [] = + fun depth (bnd, inc) [] = if bnd > lim then - (if !trace_DEPTH_FIRST then - tracing (string_of_int (!countr) ^ - " inferences so far. Giving up at " ^ - string_of_int bnd) - else (); - NONE) + (if !trace_DEPTH_FIRST then + tracing (string_of_int (! countr) ^ + " inferences so far. Giving up at " ^ string_of_int bnd) + else (); + NONE) else - (if !trace_DEPTH_FIRST then - tracing (string_of_int (!countr) ^ - " inferences so far. Searching to depth " ^ - string_of_int bnd) - else (); - (*larger increments make it run slower for the hard problems*) - depth (bnd+inc, 10)) [(0, 1, false, qs0)] - | depth (bnd,inc) ((k,np,rgd,q)::qs) = - if k>=bnd then depth (bnd,inc) qs + (if !trace_DEPTH_FIRST then + tracing (string_of_int (!countr) ^ + " inferences so far. Searching to depth " ^ string_of_int bnd) + else (); + (*larger increments make it run slower for the hard problems*) + depth (bnd + inc, 10)) [(0, 1, false, qs0)] + | depth (bnd, inc) ((k, np, rgd, q) :: qs) = + if k >= bnd then depth (bnd, inc) qs else - case (Unsynchronized.inc countr; - if !trace_DEPTH_FIRST then - tracing (string_of_int np ^ implode (map (fn _ => "*") qs)) - else (); - Seq.pull q) of - NONE => depth (bnd,inc) qs - | SOME(st,stq) => - if satp st (*solution!*) - then SOME(st, Seq.make - (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs))) - - else - let val np' = Thm.nprems_of st - (*rgd' calculation assumes tactic operates on subgoal 1*) - val rgd' = not (has_vars (hd (Thm.prems_of st))) - val k' = k+np'-np+1 (*difference in # of subgoals, +1*) - in if k'+np' >= bnd - then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs - else if np' < np (*solved a subgoal; prune rigid ancestors*) - then depth (bnd,inc) - (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs)) - else depth (bnd,inc) ((k', np', rgd', tf st) :: - (k,np,rgd,stq) :: qs) - end - in depth (0,5) [] end); + (case + (Unsynchronized.inc countr; + if !trace_DEPTH_FIRST then + tracing (string_of_int np ^ implode (map (fn _ => "*") qs)) + else (); + Seq.pull q) of + NONE => depth (bnd, inc) qs + | SOME (st, stq) => + if satp st then (*solution!*) + SOME(st, Seq.make (fn() => depth (bnd, inc) ((k, np, rgd, stq) :: qs))) + else + let + val np' = Thm.nprems_of st; + (*rgd' calculation assumes tactic operates on subgoal 1*) + val rgd' = not (has_vars (hd (Thm.prems_of st))); + val k' = k + np' - np + 1; (*difference in # of subgoals, +1*) + in + if k' + np' >= bnd then depth (bnd, Int.min (inc, k' + np' + 1 - bnd)) qs + else if np' < np (*solved a subgoal; prune rigid ancestors*) + then depth (bnd, inc) (prune ((k', np', rgd', tf st), (k, np, rgd, stq) :: qs)) + else depth (bnd, inc) ((k', np', rgd', tf st) :: (k, np, rgd, stq) :: qs) + end) + in depth (0, 5) [] end); fun ITER_DEEPEN lim = THEN_ITER_DEEPEN lim all_tac; @@ -200,8 +197,8 @@ val trace_BEST_FIRST = Unsynchronized.ref false; (*For creating output sequence*) -fun some_of_list [] = NONE - | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l)); +fun some_of_list [] = NONE + | some_of_list (x :: l) = SOME (x, Seq.make (fn () => some_of_list l)); (*Check for and delete duplicate proof states*) fun delete_all_min prf heap = @@ -214,23 +211,26 @@ Function sizef estimates size of problem remaining (smaller means better). tactic tac0 sets up the initial priority queue, while tac1 searches it. *) fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = - let val tac = tracify trace_BEST_FIRST tac1 - fun pairsize th = (sizef th, th); - fun bfs (news,nprf_heap) = - (case List.partition satp news of - ([],nonsats) => next(fold_rev Thm_Heap.insert (map pairsize nonsats) nprf_heap) - | (sats,_) => some_of_list sats) - and next nprf_heap = - if Thm_Heap.is_empty nprf_heap then NONE - else - let val (n,prf) = Thm_Heap.min nprf_heap - in if !trace_BEST_FIRST - then tracing("state size = " ^ string_of_int n) - else (); - bfs (Seq.list_of (tac prf), - delete_all_min prf (Thm_Heap.delete_min nprf_heap)) - end - fun btac st = bfs (Seq.list_of (tac0 st), Thm_Heap.empty) + let + val tac = tracify trace_BEST_FIRST tac1; + fun pairsize th = (sizef th, th); + fun bfs (news, nprf_heap) = + (case List.partition satp news of + ([], nonsats) => next (fold_rev Thm_Heap.insert (map pairsize nonsats) nprf_heap) + | (sats, _) => some_of_list sats) + and next nprf_heap = + if Thm_Heap.is_empty nprf_heap then NONE + else + let + val (n, prf) = Thm_Heap.min nprf_heap; + val _ = + if !trace_BEST_FIRST + then tracing("state size = " ^ string_of_int n) + else (); + in + bfs (Seq.list_of (tac prf), delete_all_min prf (Thm_Heap.delete_min nprf_heap)) + end; + fun btac st = bfs (Seq.list_of (tac0 st), Thm_Heap.empty) in traced_tac btac end; (*Ordinary best-first search, with no initial tactic*) @@ -238,59 +238,59 @@ (*Breadth-first search to satisfy satpred (including initial state) SLOW -- SHOULD NOT USE APPEND!*) -fun gen_BREADTH_FIRST message satpred (tac:tactic) = - let val tacf = Seq.list_of o tac; - fun bfs prfs = - (case List.partition satpred prfs of - ([],[]) => [] - | ([],nonsats) => - (message("breadth=" ^ string_of_int(length nonsats)); - bfs (maps tacf nonsats)) - | (sats,_) => sats) - in (fn st => Seq.of_list (bfs [st])) end; +fun gen_BREADTH_FIRST message satpred (tac: tactic) = + let + val tacf = Seq.list_of o tac; + fun bfs prfs = + (case List.partition satpred prfs of + ([], []) => [] + | ([], nonsats) => + (message ("breadth=" ^ string_of_int (length nonsats)); + bfs (maps tacf nonsats)) + | (sats, _) => sats); + in fn st => Seq.of_list (bfs [st]) end; val BREADTH_FIRST = gen_BREADTH_FIRST tracing; val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ()); -(* Author: Norbert Voelker, FernUniversitaet Hagen - Remarks: Implementation of A*-like proof procedure by modification - of the existing code for BEST_FIRST and best_tac so that the - current level of search is taken into account. +(* + Implementation of A*-like proof procedure by modification + of the existing code for BEST_FIRST and best_tac so that the + current level of search is taken into account. *) -(*Insertion into priority queue of states, marked with level *) -fun insert_with_level (lnth: int*int*thm) [] = [lnth] - | insert_with_level (l,m,th) ((l',n,th') :: nths) = - if n some_of_list l)); +fun some_of_list [] = NONE + | some_of_list (x :: xs) = SOME (x, Seq.make (fn () => some_of_list xs)); val trace_ASTAR = Unsynchronized.ref false; fun THEN_ASTAR tac0 (satp, costf) tac1 = - let val tf = tracify trace_ASTAR tac1; - fun bfs (news,nprfs,level) = - let fun cost thm = (level, costf level thm, thm) - in (case List.partition satp news of - ([],nonsats) - => next (fold_rev (insert_with_level o cost) nonsats nprfs) - | (sats,_) => some_of_list sats) - end and - next [] = NONE - | next ((level,n,prf)::nprfs) = - (if !trace_ASTAR - then tracing("level = " ^ string_of_int level ^ - " cost = " ^ string_of_int n ^ - " queue length =" ^ string_of_int (length nprfs)) - else (); - bfs (Seq.list_of (tf prf), nprfs,level+1)) - fun tf st = bfs (Seq.list_of (tac0 st), [], 0) + let + val tf = tracify trace_ASTAR tac1; + fun bfs (news, nprfs, level) = + let fun cost thm = (level, costf level thm, thm) in + (case List.partition satp news of + ([], nonsats) => next (fold_rev (insert_with_level o cost) nonsats nprfs) + | (sats, _) => some_of_list sats) + end + and next [] = NONE + | next ((level, n, prf) :: nprfs) = + (if !trace_ASTAR then + tracing ("level = " ^ string_of_int level ^ + " cost = " ^ string_of_int n ^ + " queue length =" ^ string_of_int (length nprfs)) + else (); + bfs (Seq.list_of (tf prf), nprfs, level + 1)) + fun tf st = bfs (Seq.list_of (tac0 st), [], 0); in traced_tac tf end; (*Ordinary ASTAR, with no initial tactic*)