1.1 --- a/src/Provers/blast.ML Sun Jul 29 19:46:02 2007 +0200
1.2 +++ b/src/Provers/blast.ML Sun Jul 29 19:46:03 2007 +0200
1.3 @@ -85,17 +85,13 @@
1.4 val trace : bool ref
1.5 val fullTrace : branch list list ref
1.6 val fromType : (indexname * term) list ref -> Term.typ -> term
1.7 - val fromTerm : Term.term -> term
1.8 - val fromSubgoal : Term.term -> term
1.9 + val fromTerm : theory -> Term.term -> term
1.10 + val fromSubgoal : theory -> Term.term -> term
1.11 val instVars : term -> (unit -> unit)
1.12 val toTerm : int -> term -> Term.term
1.13 val readGoal : theory -> string -> term
1.14 val tryInThy : theory -> int -> string ->
1.15 (int->tactic) list * branch list list * (int*int*exn) list
1.16 - val trygl : claset -> int -> int ->
1.17 - (int->tactic) list * branch list list * (int*int*exn) list
1.18 - val Trygl : int -> int ->
1.19 - (int->tactic) list * branch list list * (int*int*exn) list
1.20 val normBr : branch -> branch
1.21 end;
1.22
1.23 @@ -117,6 +113,41 @@
1.24 | Abs of string*term
1.25 | op $ of term*term;
1.26
1.27 +(*Pending formulae carry md (may duplicate) flags*)
1.28 +type branch =
1.29 + {pairs: ((term*bool) list * (*safe formulae on this level*)
1.30 + (term*bool) list) list, (*haz formulae on this level*)
1.31 + lits: term list, (*literals: irreducible formulae*)
1.32 + vars: term option ref list, (*variables occurring in branch*)
1.33 + lim: int}; (*resource limit*)
1.34 +
1.35 +
1.36 +(* global state information *)
1.37 +
1.38 +datatype state = State of
1.39 + {thy: theory,
1.40 + fullTrace: branch list list ref,
1.41 + trail: term option ref list ref,
1.42 + ntrail: int ref,
1.43 + nclosed: int ref,
1.44 + ntried: int ref}
1.45 +
1.46 +fun reject_const thy c =
1.47 + is_some (Sign.const_type thy c) andalso
1.48 + error ("blast: theory contains illegal constant " ^ quote c);
1.49 +
1.50 +fun initialize thy =
1.51 + (reject_const thy "*Goal*";
1.52 + reject_const thy "*False*";
1.53 + State
1.54 + {thy = thy,
1.55 + fullTrace = ref [],
1.56 + trail = ref [],
1.57 + ntrail = ref 0,
1.58 + nclosed = ref 0, (*branches closed: number of branches closed during the search*)
1.59 + ntried = ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*)
1.60 +
1.61 +
1.62
1.63 (** Basic syntactic operations **)
1.64
1.65 @@ -176,11 +207,8 @@
1.66 end
1.67 | SOME v => v)
1.68
1.69 -(*refer to the theory in which blast is initialized*)
1.70 -val typargs = ref (fn ((_, T): string * typ) => [T]);
1.71 -
1.72 -fun fromConst alist (a, T) =
1.73 - Const (a, map (fromType alist) (! typargs (a, T)));
1.74 +fun fromConst thy alist (a, T) =
1.75 + Const (a, map (fromType alist) (Sign.const_typargs thy (a, T)));
1.76
1.77
1.78 (*Tests whether 2 terms are alpha-convertible; chases instantiations*)
1.79 @@ -324,12 +352,9 @@
1.80
1.81 exception UNIFY;
1.82
1.83 -val trail = ref [] : term option ref list ref;
1.84 -val ntrail = ref 0;
1.85 -
1.86
1.87 (*Restore the trail to some previous state: for backtracking*)
1.88 -fun clearTo n =
1.89 +fun clearTo (State {ntrail, trail, ...}) n =
1.90 while !ntrail<>n do
1.91 (hd(!trail) := NONE;
1.92 trail := tl (!trail);
1.93 @@ -340,8 +365,9 @@
1.94 "vars" is a list of variables local to the rule and NOT to be put
1.95 on the trail (no point in doing so)
1.96 *)
1.97 -fun unify(vars,t,u) =
1.98 - let val n = !ntrail
1.99 +fun unify state (vars,t,u) =
1.100 + let val State {ntrail, trail, ...} = state
1.101 + val n = !ntrail
1.102 fun update (t as Var v, u) =
1.103 if t aconv u then ()
1.104 else if varOccur v u then raise UNIFY
1.105 @@ -364,16 +390,16 @@
1.106 and unifysAux ([], []) = ()
1.107 | unifysAux (t :: ts, u :: us) = (unifyAux (t, u); unifysAux (ts, us))
1.108 | unifysAux _ = raise UNIFY;
1.109 - in (unifyAux(t,u); true) handle UNIFY => (clearTo n; false)
1.110 + in (unifyAux(t,u); true) handle UNIFY => (clearTo state n; false)
1.111 end;
1.112
1.113
1.114 (*Convert from "real" terms to prototerms; eta-contract.
1.115 Code is similar to fromSubgoal.*)
1.116 -fun fromTerm t =
1.117 +fun fromTerm thy t =
1.118 let val alistVar = ref []
1.119 and alistTVar = ref []
1.120 - fun from (Term.Const aT) = fromConst alistTVar aT
1.121 + fun from (Term.Const aT) = fromConst thy alistTVar aT
1.122 | from (Term.Free (a,_)) = Free a
1.123 | from (Term.Bound i) = Bound i
1.124 | from (Term.Var (ixn,T)) =
1.125 @@ -479,8 +505,8 @@
1.126 (*Tableau rule from elimination rule.
1.127 Flag "upd" says that the inference updated the branch.
1.128 Flag "dup" requests duplication of the affected formula.*)
1.129 -fun fromRule vars rl =
1.130 - let val trl = rl |> Thm.prop_of |> fromTerm |> convertRule vars
1.131 +fun fromRule thy vars rl =
1.132 + let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars
1.133 fun tac (upd, dup,rot) i =
1.134 emtac upd (if dup then rev_dup_elim rl else rl) i
1.135 THEN
1.136 @@ -511,8 +537,8 @@
1.137 Flag "dup" requests duplication of the affected formula.
1.138 Since haz rules are now delayed, "dup" is always FALSE for
1.139 introduction rules.*)
1.140 -fun fromIntrRule vars rl =
1.141 - let val trl = rl |> Thm.prop_of |> fromTerm |> convertIntrRule vars
1.142 +fun fromIntrRule thy vars rl =
1.143 + let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
1.144 fun tac (upd,dup,rot) i =
1.145 rmtac upd (if dup then Data.dup_intr rl else rl) i
1.146 THEN
1.147 @@ -534,28 +560,18 @@
1.148 | toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u);
1.149
1.150
1.151 -fun netMkRules P vars (nps: netpair list) =
1.152 +fun netMkRules thy P vars (nps: netpair list) =
1.153 case P of
1.154 (Const ("*Goal*", _) $ G) =>
1.155 let val pG = mk_Trueprop (toTerm 2 G)
1.156 val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
1.157 - in map (fromIntrRule vars o #2) (Tactic.orderlist intrs) end
1.158 + in map (fromIntrRule thy vars o #2) (Tactic.orderlist intrs) end
1.159 | _ =>
1.160 let val pP = mk_Trueprop (toTerm 3 P)
1.161 val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
1.162 - in map_filter (fromRule vars o #2) (Tactic.orderlist elims) end;
1.163 + in map_filter (fromRule thy vars o #2) (Tactic.orderlist elims) end;
1.164
1.165
1.166 -(*Pending formulae carry md (may duplicate) flags*)
1.167 -type branch =
1.168 - {pairs: ((term*bool) list * (*safe formulae on this level*)
1.169 - (term*bool) list) list, (*haz formulae on this level*)
1.170 - lits: term list, (*literals: irreducible formulae*)
1.171 - vars: term option ref list, (*variables occurring in branch*)
1.172 - lim: int}; (*resource limit*)
1.173 -
1.174 -val fullTrace = ref[] : branch list list ref;
1.175 -
1.176 (*Normalize a branch--for tracing*)
1.177 fun norm2 (G,md) = (norm G, md);
1.178
1.179 @@ -598,7 +614,7 @@
1.180 | showTerm d (f $ u) = if d=0 then dummyVar
1.181 else Term.$ (showTerm d f, showTerm (d-1) u);
1.182
1.183 -fun string_of sign d t = Sign.string_of_term sign (showTerm d t);
1.184 +fun string_of thy d t = Sign.string_of_term thy (showTerm d t);
1.185
1.186 (*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like
1.187 Ex(P) is duplicated as the assumption ~Ex(P). *)
1.188 @@ -616,20 +632,20 @@
1.189 fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
1.190 rotate_tac ~1 i;
1.191
1.192 -fun traceTerm sign t =
1.193 +fun traceTerm thy t =
1.194 let val t' = norm (negOfGoal t)
1.195 - val stm = string_of sign 8 t'
1.196 + val stm = string_of thy 8 t'
1.197 in
1.198 - case topType sign t' of
1.199 + case topType thy t' of
1.200 NONE => stm (*no type to attach*)
1.201 - | SOME T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
1.202 + | SOME T => stm ^ "\t:: " ^ Sign.string_of_typ thy T
1.203 end;
1.204
1.205
1.206 (*Print tracing information at each iteration of prover*)
1.207 -fun tracing sign brs =
1.208 - let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm sign G)
1.209 - | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm sign H ^ "\t (Unsafe)")
1.210 +fun tracing (State {thy, fullTrace, ...}) brs =
1.211 + let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm thy G)
1.212 + | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm thy H ^ "\t (Unsafe)")
1.213 | printPairs _ = ()
1.214 fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
1.215 (fullTrace := brs0 :: !fullTrace;
1.216 @@ -643,14 +659,14 @@
1.217 fun traceMsg s = if !trace then writeln s else ();
1.218
1.219 (*Tracing: variables updated in the last branch operation?*)
1.220 -fun traceVars sign ntrl =
1.221 +fun traceVars (State {thy, ntrail, trail, ...}) ntrl =
1.222 if !trace then
1.223 (case !ntrail-ntrl of
1.224 0 => ()
1.225 | 1 => Output.immediate_output"\t1 variable UPDATED:"
1.226 | n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
1.227 (*display the instantiations themselves, though no variable names*)
1.228 - List.app (fn v => Output.immediate_output(" " ^ string_of sign 4 (the (!v))))
1.229 + List.app (fn v => Output.immediate_output(" " ^ string_of thy 4 (the (!v))))
1.230 (List.take(!trail, !ntrail-ntrl));
1.231 writeln"")
1.232 else ();
1.233 @@ -736,7 +752,7 @@
1.234 (*Substitute through the branch if an equality goal (else raise DEST_EQ).
1.235 Moves affected literals back into the branch, but it is not clear where
1.236 they should go: this could make proofs fail.*)
1.237 -fun equalSubst sign (G, {pairs, lits, vars, lim}) =
1.238 +fun equalSubst thy (G, {pairs, lits, vars, lim}) =
1.239 let val (t,u) = orientGoal(dest_eq G)
1.240 val subst = subst_atomic (t,u)
1.241 fun subst2(G,md) = (subst G, md)
1.242 @@ -759,8 +775,8 @@
1.243 end
1.244 val (changed, lits') = foldr subLit ([], []) lits
1.245 val (changed', pairs') = foldr subFrame (changed, []) pairs
1.246 - in if !trace then writeln ("Substituting " ^ traceTerm sign u ^
1.247 - " for " ^ traceTerm sign t ^ " in branch" )
1.248 + in if !trace then writeln ("Substituting " ^ traceTerm thy u ^
1.249 + " for " ^ traceTerm thy t ^ " in branch" )
1.250 else ();
1.251 {pairs = (changed',[])::pairs', (*affected formulas, and others*)
1.252 lits = lits', (*unaffected literals*)
1.253 @@ -781,9 +797,9 @@
1.254 val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac);
1.255
1.256 (*Try to unify complementary literals and return the corresponding tactic. *)
1.257 -fun tryClose (G, L) =
1.258 +fun tryClose state (G, L) =
1.259 let
1.260 - fun close t u tac = if unify ([], t, u) then SOME tac else NONE;
1.261 + fun close t u tac = if unify state ([], t, u) then SOME tac else NONE;
1.262 fun arg (_ $ t) = t;
1.263 in
1.264 if isGoal G then close (arg G) L eAssume_tac
1.265 @@ -820,9 +836,9 @@
1.266 (*nbrs = # of branches just prior to closing this one. Delete choice points
1.267 for goals proved by the latest inference, provided NO variables in the
1.268 next branch have been updated.*)
1.269 -fun prune (1, nxtVars, choices) = choices (*DON'T prune at very end: allow
1.270 +fun prune _ (1, nxtVars, choices) = choices (*DON'T prune at very end: allow
1.271 backtracking over bad proofs*)
1.272 - | prune (nbrs: int, nxtVars, choices) =
1.273 + | prune (State {ntrail, trail, ...}) (nbrs: int, nxtVars, choices) =
1.274 let fun traceIt last =
1.275 let val ll = length last
1.276 and lc = length choices
1.277 @@ -895,12 +911,7 @@
1.278 | matchs (t :: ts) (u :: us) = match t u andalso matchs ts us;
1.279
1.280
1.281 -(*Branches closed: number of branches closed during the search
1.282 - Branches tried: number of branches created by splitting (counting from 1)*)
1.283 -val nclosed = ref 0
1.284 -and ntried = ref 1;
1.285 -
1.286 -fun printStats (b, start, tacs) =
1.287 +fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
1.288 if b then
1.289 writeln (end_timing start ^ " for search. Closed: "
1.290 ^ Int.toString (!nclosed) ^
1.291 @@ -914,12 +925,13 @@
1.292 bound on unsafe expansions.
1.293 "start" is CPU time at start, for printing search time
1.294 *)
1.295 -fun prove (sign, start, cs, brs, cont) =
1.296 - let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
1.297 +fun prove (state, start, cs, brs, cont) =
1.298 + let val State {thy, ntrail, nclosed, ntried, ...} = state;
1.299 + val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
1.300 val safeList = [safe0_netpair, safep_netpair]
1.301 and hazList = [haz_netpair]
1.302 fun prv (tacs, trs, choices, []) =
1.303 - (printStats (!trace orelse !stats, start, tacs);
1.304 + (printStats state (!trace orelse !stats, start, tacs);
1.305 cont (tacs, trs, choices)) (*all branches closed!*)
1.306 | prv (tacs, trs, choices,
1.307 brs0 as {pairs = ((G,md)::br, haz)::pairs,
1.308 @@ -931,7 +943,7 @@
1.309 val nbrs = length brs0
1.310 val nxtVars = nextVars brs
1.311 val G = norm G
1.312 - val rules = netMkRules G vars safeList
1.313 + val rules = netMkRules thy G vars safeList
1.314 (*Make a new branch, decrementing "lim" if instantiations occur*)
1.315 fun newBr (vars',lim') prems =
1.316 map (fn prem =>
1.317 @@ -952,7 +964,7 @@
1.318 to branch.*)
1.319 fun deeper [] = raise NEWBRANCHES
1.320 | deeper (((P,prems),tac)::grls) =
1.321 - if unify(add_term_vars(P,[]), P, G)
1.322 + if unify state (add_term_vars(P,[]), P, G)
1.323 then (*P comes from the rule; G comes from the branch.*)
1.324 let val updated = ntrl < !ntrail (*branch updated*)
1.325 val lim' = if updated
1.326 @@ -964,16 +976,16 @@
1.327 val tacs' = (tac(updated,false,true))
1.328 :: tacs (*no duplication; rotate*)
1.329 in
1.330 - traceNew prems; traceVars sign ntrl;
1.331 + traceNew prems; traceVars state ntrl;
1.332 (if null prems then (*closed the branch: prune!*)
1.333 (nclosed := !nclosed + 1;
1.334 prv(tacs', brs0::trs,
1.335 - prune (nbrs, nxtVars, choices'),
1.336 + prune state (nbrs, nxtVars, choices'),
1.337 brs))
1.338 else (*prems non-null*)
1.339 if lim'<0 (*faster to kill ALL the alternatives*)
1.340 then (traceMsg"Excessive branching: KILLED";
1.341 - clearTo ntrl; raise NEWBRANCHES)
1.342 + clearTo state ntrl; raise NEWBRANCHES)
1.343 else
1.344 (ntried := !ntried + length prems - 1;
1.345 prv(tacs', brs0::trs, choices',
1.346 @@ -982,7 +994,7 @@
1.347 if updated then
1.348 (*Backtrack at this level.
1.349 Reset Vars and try another rule*)
1.350 - (clearTo ntrl; deeper grls)
1.351 + (clearTo state ntrl; deeper grls)
1.352 else (*backtrack to previous level*)
1.353 backtrack choices
1.354 end
1.355 @@ -990,21 +1002,21 @@
1.356 (*Try to close branch by unifying with head goal*)
1.357 fun closeF [] = raise CLOSEF
1.358 | closeF (L::Ls) =
1.359 - case tryClose(G,L) of
1.360 + case tryClose state (G,L) of
1.361 NONE => closeF Ls
1.362 | SOME tac =>
1.363 let val choices' =
1.364 (if !trace then (Output.immediate_output"branch closed";
1.365 - traceVars sign ntrl)
1.366 + traceVars state ntrl)
1.367 else ();
1.368 - prune (nbrs, nxtVars,
1.369 + prune state (nbrs, nxtVars,
1.370 (ntrl, nbrs, PRV) :: choices))
1.371 in nclosed := !nclosed + 1;
1.372 prv (tac::tacs, brs0::trs, choices', brs)
1.373 handle PRV =>
1.374 (*reset Vars and try another literal
1.375 [this handler is pruned if possible!]*)
1.376 - (clearTo ntrl; closeF Ls)
1.377 + (clearTo state ntrl; closeF Ls)
1.378 end
1.379 (*Try to unify a queued formula (safe or haz) with head goal*)
1.380 fun closeFl [] = raise CLOSEF
1.381 @@ -1012,12 +1024,12 @@
1.382 closeF (map fst br)
1.383 handle CLOSEF => closeF (map fst haz)
1.384 handle CLOSEF => closeFl pairs
1.385 - in tracing sign brs0;
1.386 + in tracing state brs0;
1.387 if lim<0 then (traceMsg "Limit reached. "; backtrack choices)
1.388 else
1.389 prv (Data.hyp_subst_tac (!trace) :: tacs,
1.390 brs0::trs, choices,
1.391 - equalSubst sign
1.392 + equalSubst thy
1.393 (G, {pairs = (br,haz)::pairs,
1.394 lits = lits, vars = vars, lim = lim})
1.395 :: brs)
1.396 @@ -1025,7 +1037,7 @@
1.397 handle CLOSEF => closeFl ((br,haz)::pairs)
1.398 handle CLOSEF => deeper rules
1.399 handle NEWBRANCHES =>
1.400 - (case netMkRules G vars hazList of
1.401 + (case netMkRules thy G vars hazList of
1.402 [] => (*there are no plausible haz rules*)
1.403 (traceMsg "moving formula to literals";
1.404 prv (tacs, brs0::trs, choices,
1.405 @@ -1059,7 +1071,7 @@
1.406 let exception PRV (*backtrack to precisely this recursion!*)
1.407 val H = norm H
1.408 val ntrl = !ntrail
1.409 - val rules = netMkRules H vars hazList
1.410 + val rules = netMkRules thy H vars hazList
1.411 (*new premises of haz rules may NOT be duplicated*)
1.412 fun newPrem (vars,P,dup,lim') prem =
1.413 let val Gs' = map (fn Q => (Q,false)) prem
1.414 @@ -1082,7 +1094,7 @@
1.415 to branch.*)
1.416 fun deeper [] = raise NEWBRANCHES
1.417 | deeper (((P,prems),tac)::grls) =
1.418 - if unify(add_term_vars(P,[]), P, H)
1.419 + if unify state (add_term_vars(P,[]), P, H)
1.420 then
1.421 let val updated = ntrl < !ntrail (*branch updated*)
1.422 val vars = vars_in_vars vars
1.423 @@ -1122,14 +1134,14 @@
1.424 if lim'<0 andalso not (null prems)
1.425 then (*it's faster to kill ALL the alternatives*)
1.426 (traceMsg"Excessive branching: KILLED";
1.427 - clearTo ntrl; raise NEWBRANCHES)
1.428 + clearTo state ntrl; raise NEWBRANCHES)
1.429 else
1.430 traceNew prems;
1.431 if !trace andalso dup then Output.immediate_output" (duplicating)"
1.432 else ();
1.433 if !trace andalso recur then Output.immediate_output" (recursive)"
1.434 else ();
1.435 - traceVars sign ntrl;
1.436 + traceVars state ntrl;
1.437 if null prems then nclosed := !nclosed + 1
1.438 else ntried := !ntried + length prems - 1;
1.439 prv(tac' :: tacs,
1.440 @@ -1139,12 +1151,12 @@
1.441 handle PRV =>
1.442 if mayUndo
1.443 then (*reset Vars and try another rule*)
1.444 - (clearTo ntrl; deeper grls)
1.445 + (clearTo state ntrl; deeper grls)
1.446 else (*backtrack to previous level*)
1.447 backtrack choices
1.448 end
1.449 else deeper grls
1.450 - in tracing sign brs0;
1.451 + in tracing state brs0;
1.452 if lim<1 then (traceMsg "Limit reached. "; backtrack choices)
1.453 else deeper rules
1.454 handle NEWBRANCHES =>
1.455 @@ -1185,7 +1197,7 @@
1.456 exception TRANS of string;
1.457
1.458 (*Translation of a subgoal: Skolemize all parameters*)
1.459 -fun fromSubgoal t =
1.460 +fun fromSubgoal thy t =
1.461 let val alistVar = ref []
1.462 and alistTVar = ref []
1.463 fun hdvar ((ix,(v,is))::_) = v
1.464 @@ -1201,7 +1213,7 @@
1.465 "Function unknown's argument not a bound variable"
1.466 in
1.467 case ht of
1.468 - Term.Const aT => apply (fromConst alistTVar aT)
1.469 + Term.Const aT => apply (fromConst thy alistTVar aT)
1.470 | Term.Free (a,_) => apply (Free a)
1.471 | Term.Bound i => apply (Bound i)
1.472 | Term.Var (ix,_) =>
1.473 @@ -1231,25 +1243,15 @@
1.474 in skoSubgoal 0 (from 0 (discard_foralls t)) end;
1.475
1.476
1.477 -fun reject_const thy c =
1.478 - if is_some (Sign.const_type thy c) then
1.479 - error ("Blast: theory contains illegal constant " ^ quote c)
1.480 - else ();
1.481 -
1.482 -fun initialize thy =
1.483 - (fullTrace:=[]; trail := []; ntrail := 0;
1.484 - nclosed := 0; ntried := 1; typargs := Sign.const_typargs thy;
1.485 - reject_const thy "*Goal*"; reject_const thy "*False*");
1.486 -
1.487 -
1.488 (*Tactic using tableau engine and proof reconstruction.
1.489 "start" is CPU time at start, for printing SEARCH time
1.490 (also prints reconstruction time)
1.491 "lim" is depth limit.*)
1.492 -fun timing_depth_tac start cs lim i st0 = NAMED_CRITICAL "blast" (fn () =>
1.493 - let val st = (initialize (theory_of_thm st0); Conv.gconv_rule ObjectLogic.atomize_prems i st0);
1.494 - val sign = Thm.theory_of_thm st
1.495 - val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
1.496 +fun timing_depth_tac start cs lim i st0 =
1.497 + let val thy = Thm.theory_of_thm st0
1.498 + val state = initialize thy
1.499 + val st = Conv.gconv_rule ObjectLogic.atomize_prems i st0
1.500 + val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1))
1.501 val hyps = strip_imp_prems skoprem
1.502 and concl = strip_imp_concl skoprem
1.503 fun cont (tacs,_,choices) =
1.504 @@ -1266,10 +1268,8 @@
1.505 else ();
1.506 Seq.make(fn()=> cell))
1.507 end
1.508 - val forced = Seq.pull
1.509 - (prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont))
1.510 - in Seq.make (fn () => forced) end
1.511 - handle PROVE => Seq.empty);
1.512 + in prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end
1.513 + handle PROVE => Seq.empty
1.514
1.515 (*Public version with fixed depth*)
1.516 fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
1.517 @@ -1289,31 +1289,18 @@
1.518 (*** For debugging: these apply the prover to a subgoal and return
1.519 the resulting tactics, trace, etc. ***)
1.520
1.521 -(*Translate subgoal i from a proof state*)
1.522 -fun trygl cs lim i =
1.523 - let val st = topthm()
1.524 - val sign = Thm.theory_of_thm st
1.525 - val skoprem = (initialize (theory_of_thm st);
1.526 - fromSubgoal (List.nth(prems_of st, i-1)))
1.527 - val hyps = strip_imp_prems skoprem
1.528 - and concl = strip_imp_concl skoprem
1.529 - in timeap prove (sign, start_timing (), cs,
1.530 - [initBranch (mkGoal concl :: hyps, lim)], I)
1.531 - end
1.532 - handle Subscript => error("There is no subgoal " ^ Int.toString i);
1.533 -
1.534 -fun Trygl lim i = trygl (Data.claset()) lim i;
1.535 +val fullTrace = ref ([]: branch list list);
1.536
1.537 (*Read a string to make an initial, singleton branch*)
1.538 -fun readGoal thy s = Sign.read_prop thy s |> fromTerm |> rand |> mkGoal;
1.539 +fun readGoal thy s = Sign.read_prop thy s |> fromTerm thy |> rand |> mkGoal;
1.540
1.541 fun tryInThy thy lim s =
1.542 - (initialize thy;
1.543 - timeap prove (thy,
1.544 - start_timing(),
1.545 - Data.claset(),
1.546 - [initBranch ([readGoal thy s], lim)],
1.547 - I));
1.548 + let
1.549 + val state as State {fullTrace = ft, ...} = initialize thy;
1.550 + val res = timeap prove
1.551 + (state, start_timing(), Data.claset(), [initBranch ([readGoal thy s], lim)], I);
1.552 + val _ = fullTrace := !ft;
1.553 + in res end;
1.554
1.555
1.556 (** method setup **)