# HG changeset patch # User wenzelm # Date 1307711009 -7200 # Node ID 00db2eed718968b1f0801d38653eebb2e9f38164 # Parent 396aaa15dd8bbd9d779e6723134ab71858fbb455# Parent 5fcd0ca1f58272a1655b0bd06c36ef952d413727 merged diff -r 396aaa15dd8b -r 00db2eed7189 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Fri Jun 10 12:01:15 2011 +0200 +++ b/Admin/isatest/isatest-makedist Fri Jun 10 15:03:29 2011 +0200 @@ -98,7 +98,7 @@ ## spawn test runs -$SSH macbroy21 "$MAKEALL $HOME/settings/at-poly-test" +$SSH macbroy20 "$MAKEALL $HOME/settings/at-poly-test" # give test some time to copy settings and start sleep 15 $SSH macbroy28 "$MAKEALL $HOME/settings/at-poly" diff -r 396aaa15dd8b -r 00db2eed7189 Admin/isatest/settings/at-poly-test --- a/Admin/isatest/settings/at-poly-test Fri Jun 10 12:01:15 2011 +0200 +++ b/Admin/isatest/settings/at-poly-test Fri Jun 10 15:03:29 2011 +0200 @@ -24,7 +24,7 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true" -ISABELLE_GHC="/home/isabelle/contrib_devel/ghc/x86-linux/ghc" +ISABELLE_GHC="/usr/bin/ghc" ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml" ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl" diff -r 396aaa15dd8b -r 00db2eed7189 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Jun 10 12:01:15 2011 +0200 +++ b/src/Provers/blast.ML Fri Jun 10 15:03:29 2011 +0200 @@ -59,22 +59,15 @@ | $ of term*term; val depth_tac: Proof.context -> int -> int -> tactic val depth_limit: int Config.T + val trace: bool Config.T + val stats: bool Config.T val blast_tac: Proof.context -> int -> tactic val setup: theory -> theory (*debugging tools*) type branch - val stats: bool Config.T - val trace: bool Config.T - val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term - val fromTerm: theory -> Term.term -> term - val fromSubgoal: theory -> Term.term -> term - val instVars: term -> (unit -> unit) - val toTerm: int -> term -> Term.term - val readGoal: Proof.context -> string -> term val tryIt: Proof.context -> int -> string -> {fullTrace: branch list list, result: ((int -> tactic) list * branch list list * (int * int * exn) list)} - val normBr: branch -> branch end; functor Blast(Data: BLAST_DATA): BLAST = @@ -82,9 +75,12 @@ structure Classical = Data.Classical; -val trace = Config.bool (Config.declare "Blast.trace" (K (Config.Bool false))); -val stats = Config.bool (Config.declare "Blast.stats" (K (Config.Bool false))); -(*for runtime and search statistics*) +(* options *) + +val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20); +val (trace, setup_trace) = Attrib.config_bool @{binding blast_trace} (K false); +val (stats, setup_stats) = Attrib.config_bool @{binding blast_stats} (K false); + datatype term = Const of string * term list (*typargs constant--as a terms!*) @@ -108,6 +104,7 @@ datatype state = State of {ctxt: Proof.context, + names: Name.context Unsynchronized.ref, fullTrace: branch list list Unsynchronized.ref, trail: term option Unsynchronized.ref list Unsynchronized.ref, ntrail: int Unsynchronized.ref, @@ -126,6 +123,7 @@ in State {ctxt = ctxt, + names = Unsynchronized.ref (Variable.names_of ctxt), fullTrace = Unsynchronized.ref [], trail = Unsynchronized.ref [], ntrail = Unsynchronized.ref 0, @@ -133,6 +131,8 @@ ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*) end; +fun gensym (State {names, ...}) x = + Unsynchronized.change_result names (Name.variant x); (** Basic syntactic operations **) @@ -443,19 +443,19 @@ else P :: delete_concl Ps | _ => P :: delete_concl Ps); -fun skoPrem vars (Const ("all", _) $ Abs (_, P)) = - skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P)) - | skoPrem vars P = P; +fun skoPrem state vars (Const ("all", _) $ Abs (_, P)) = + skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P)) + | skoPrem _ _ P = P; fun convertPrem t = delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); (*Expects elimination rules to have a formula variable as conclusion*) -fun convertRule vars t = +fun convertRule state vars t = let val (P::Ps) = strip_imp_prems t val Var v = strip_imp_concl t in v := SOME (Const ("*False*", [])); - (P, map (convertPrem o skoPrem vars) Ps) + (P, map (convertPrem o skoPrem state vars) Ps) end handle Bind => raise ElimBadConcl; @@ -492,9 +492,9 @@ (*Tableau rule from elimination rule. Flag "upd" says that the inference updated the branch. Flag "dup" requests duplication of the affected formula.*) -fun fromRule ctxt vars rl = +fun fromRule (state as State {ctxt, ...}) vars rl = let val thy = Proof_Context.theory_of ctxt - val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars + val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule state vars fun tac (upd, dup,rot) i = emtac ctxt upd (if dup then rev_dup_elim rl else rl) i THEN @@ -516,10 +516,10 @@ fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t; -fun convertIntrRule vars t = +fun convertIntrRule state vars t = let val Ps = strip_imp_prems t val P = strip_imp_concl t - in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) + in (mkGoal P, map (convertIntrPrem o skoPrem state vars) Ps) end; (*Tableau rule from introduction rule. @@ -527,9 +527,9 @@ Flag "dup" requests duplication of the affected formula. Since haz rules are now delayed, "dup" is always FALSE for introduction rules.*) -fun fromIntrRule ctxt vars rl = +fun fromIntrRule (state as State {ctxt, ...}) vars rl = let val thy = Proof_Context.theory_of ctxt - val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars + val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule state vars fun tac (upd,dup,rot) i = rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i THEN @@ -551,16 +551,16 @@ | toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u); -fun netMkRules ctxt P vars (nps: Classical.netpair list) = +fun netMkRules state P vars (nps: Classical.netpair list) = case P of (Const ("*Goal*", _) $ G) => let val pG = mk_Trueprop (toTerm 2 G) val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps - in map (fromIntrRule ctxt vars o #2) (order_list intrs) end + in map (fromIntrRule state vars o #2) (order_list intrs) end | _ => let val pP = mk_Trueprop (toTerm 3 P) val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps - in map_filter (fromRule ctxt vars o #2) (order_list elims) end; + in map_filter (fromRule state vars o #2) (order_list elims) end; (*Normalize a branch--for tracing*) @@ -936,7 +936,7 @@ val nbrs = length brs0 val nxtVars = nextVars brs val G = norm G - val rules = netMkRules ctxt G vars safeList + val rules = netMkRules state G vars safeList (*Make a new branch, decrementing "lim" if instantiations occur*) fun newBr (vars',lim') prems = map (fn prem => @@ -1030,7 +1030,7 @@ handle CLOSEF => closeFl ((br,haz)::pairs) handle CLOSEF => deeper rules handle NEWBRANCHES => - (case netMkRules ctxt G vars hazList of + (case netMkRules state G vars hazList of [] => (*there are no plausible haz rules*) (traceMsg trace "moving formula to literals"; prv (tacs, brs0::trs, choices, @@ -1064,7 +1064,7 @@ let exception PRV (*backtrack to precisely this recursion!*) val H = norm H val ntrl = !ntrail - val rules = netMkRules ctxt H vars hazList + val rules = netMkRules state H vars hazList (*new premises of haz rules may NOT be duplicated*) fun newPrem (vars,P,dup,lim') prem = let val Gs' = map (fn Q => (Q,false)) prem @@ -1188,8 +1188,9 @@ exception TRANS of string; (*Translation of a subgoal: Skolemize all parameters*) -fun fromSubgoal thy t = - let val alistVar = Unsynchronized.ref [] +fun fromSubgoal (state as State {ctxt, ...}) t = + let val thy = Proof_Context.theory_of ctxt + val alistVar = Unsynchronized.ref [] and alistTVar = Unsynchronized.ref [] fun hdvar ((ix,(v,is))::_) = v fun from lev t = @@ -1227,8 +1228,7 @@ fun skoSubgoal i t = if i (writeln ("PROOF FAILED for depth " ^ string_of_int lim); - if trace then error "************************\n" - else (); backtrack trace choices) | cell => (if (trace orelse stats) then writeln (Timing.message (Timing.result start) ^ " for reconstruction") @@ -1261,6 +1258,7 @@ end in prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont) + |> Seq.maps Thm.flexflex_rule end handle PROVE => Seq.empty | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty); @@ -1270,10 +1268,6 @@ (Object_Logic.atomize_prems_tac 1 THEN raw_blast (Timing.start ()) ctxt lim) i st; - -val (depth_limit, setup_depth_limit) = - Attrib.config_int @{binding blast_depth_limit} (K 20); - fun blast_tac ctxt i st = let val start = Timing.start (); @@ -1281,8 +1275,7 @@ in SELECT_GOAL (Object_Logic.atomize_prems_tac 1 THEN - DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1 THEN - flexflex_tac) i st + DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st end; @@ -1305,6 +1298,8 @@ val setup = setup_depth_limit #> + setup_trace #> + setup_stats #> Method.setup @{binding blast} (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >> (fn NONE => SIMPLE_METHOD' o blast_tac diff -r 396aaa15dd8b -r 00db2eed7189 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Jun 10 12:01:15 2011 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Jun 10 15:03:29 2011 +0200 @@ -420,7 +420,7 @@ val _ = Context.>> (Context.map_theory (register_config Ast.trace_raw #> - register_config Ast.stat_raw #> + register_config Ast.stats_raw #> register_config Syntax.positions_raw #> register_config Printer.show_brackets_raw #> register_config Printer.show_sorts_raw #> diff -r 396aaa15dd8b -r 00db2eed7189 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Fri Jun 10 12:01:15 2011 +0200 +++ b/src/Pure/Syntax/ast.ML Fri Jun 10 15:03:29 2011 +0200 @@ -23,8 +23,8 @@ val unfold_ast_p: string -> ast -> ast list * ast val trace_raw: Config.raw val trace: bool Config.T - val stat_raw: Config.raw - val stat: bool Config.T + val stats_raw: Config.raw + val stats: bool Config.T val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast end; @@ -167,8 +167,8 @@ val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false); val trace = Config.bool trace_raw; -val stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false); -val stat = Config.bool stat_raw; +val stats_raw = Config.declare "syntax_ast_stats" (fn _ => Config.Bool false); +val stats = Config.bool stats_raw; fun message head body = Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]); @@ -177,7 +177,7 @@ fun normalize ctxt get_rules pre_ast = let val trace = Config.get ctxt trace; - val stat = Config.get ctxt stat; + val stats = Config.get ctxt stats; val passes = Unsynchronized.ref 0; val failed_matches = Unsynchronized.ref 0; @@ -239,7 +239,7 @@ val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else (); val post_ast = normal pre_ast; val _ = - if trace orelse stat then + if trace orelse stats then tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^ string_of_int (! passes) ^ " passes, " ^ string_of_int (! changes) ^ " changes, " ^