merged
authorwenzelm
Fri Jun 10 15:03:29 2011 +0200 (2011-06-10)
changeset 4335500db2eed7189
parent 43354 396aaa15dd8b
parent 43350 5fcd0ca1f582
child 43356 2dee03f192b7
merged
     1.1 --- a/Admin/isatest/isatest-makedist	Fri Jun 10 12:01:15 2011 +0200
     1.2 +++ b/Admin/isatest/isatest-makedist	Fri Jun 10 15:03:29 2011 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4  
     1.5  ## spawn test runs
     1.6  
     1.7 -$SSH macbroy21 "$MAKEALL $HOME/settings/at-poly-test"
     1.8 +$SSH macbroy20 "$MAKEALL $HOME/settings/at-poly-test"
     1.9  # give test some time to copy settings and start
    1.10  sleep 15
    1.11  $SSH macbroy28 "$MAKEALL $HOME/settings/at-poly"
     2.1 --- a/Admin/isatest/settings/at-poly-test	Fri Jun 10 12:01:15 2011 +0200
     2.2 +++ b/Admin/isatest/settings/at-poly-test	Fri Jun 10 15:03:29 2011 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4  
     2.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
     2.6  
     2.7 -ISABELLE_GHC="/home/isabelle/contrib_devel/ghc/x86-linux/ghc"
     2.8 +ISABELLE_GHC="/usr/bin/ghc"
     2.9  ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml"
    2.10  ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl"
    2.11  
     3.1 --- a/src/Provers/blast.ML	Fri Jun 10 12:01:15 2011 +0200
     3.2 +++ b/src/Provers/blast.ML	Fri Jun 10 15:03:29 2011 +0200
     3.3 @@ -59,22 +59,15 @@
     3.4      | $  of term*term;
     3.5    val depth_tac: Proof.context -> int -> int -> tactic
     3.6    val depth_limit: int Config.T
     3.7 +  val trace: bool Config.T
     3.8 +  val stats: bool Config.T
     3.9    val blast_tac: Proof.context -> int -> tactic
    3.10    val setup: theory -> theory
    3.11    (*debugging tools*)
    3.12    type branch
    3.13 -  val stats: bool Config.T
    3.14 -  val trace: bool Config.T
    3.15 -  val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term
    3.16 -  val fromTerm: theory -> Term.term -> term
    3.17 -  val fromSubgoal: theory -> Term.term -> term
    3.18 -  val instVars: term -> (unit -> unit)
    3.19 -  val toTerm: int -> term -> Term.term
    3.20 -  val readGoal: Proof.context -> string -> term
    3.21    val tryIt: Proof.context -> int -> string ->
    3.22      {fullTrace: branch list list,
    3.23        result: ((int -> tactic) list * branch list list * (int * int * exn) list)}
    3.24 -  val normBr: branch -> branch
    3.25  end;
    3.26  
    3.27  functor Blast(Data: BLAST_DATA): BLAST =
    3.28 @@ -82,9 +75,12 @@
    3.29  
    3.30  structure Classical = Data.Classical;
    3.31  
    3.32 -val trace = Config.bool (Config.declare "Blast.trace" (K (Config.Bool false)));
    3.33 -val stats = Config.bool (Config.declare "Blast.stats" (K (Config.Bool false)));
    3.34 -(*for runtime and search statistics*)
    3.35 +(* options *)
    3.36 +
    3.37 +val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
    3.38 +val (trace, setup_trace) = Attrib.config_bool @{binding blast_trace} (K false);
    3.39 +val (stats, setup_stats) = Attrib.config_bool @{binding blast_stats} (K false);
    3.40 +
    3.41  
    3.42  datatype term =
    3.43      Const  of string * term list  (*typargs constant--as a terms!*)
    3.44 @@ -108,6 +104,7 @@
    3.45  
    3.46  datatype state = State of
    3.47   {ctxt: Proof.context,
    3.48 +  names: Name.context Unsynchronized.ref,
    3.49    fullTrace: branch list list Unsynchronized.ref,
    3.50    trail: term option Unsynchronized.ref list Unsynchronized.ref,
    3.51    ntrail: int Unsynchronized.ref,
    3.52 @@ -126,6 +123,7 @@
    3.53    in
    3.54      State
    3.55       {ctxt = ctxt,
    3.56 +      names = Unsynchronized.ref (Variable.names_of ctxt),
    3.57        fullTrace = Unsynchronized.ref [],
    3.58        trail = Unsynchronized.ref [],
    3.59        ntrail = Unsynchronized.ref 0,
    3.60 @@ -133,6 +131,8 @@
    3.61        ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*)
    3.62    end;
    3.63  
    3.64 +fun gensym (State {names, ...}) x =
    3.65 +  Unsynchronized.change_result names (Name.variant x);
    3.66  
    3.67  
    3.68  (** Basic syntactic operations **)
    3.69 @@ -443,19 +443,19 @@
    3.70            else P :: delete_concl Ps
    3.71        | _ => P :: delete_concl Ps);
    3.72  
    3.73 -fun skoPrem vars (Const ("all", _) $ Abs (_, P)) =
    3.74 -        skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
    3.75 -  | skoPrem vars P = P;
    3.76 +fun skoPrem state vars (Const ("all", _) $ Abs (_, P)) =
    3.77 +        skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P))
    3.78 +  | skoPrem _ _ P = P;
    3.79  
    3.80  fun convertPrem t =
    3.81      delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
    3.82  
    3.83  (*Expects elimination rules to have a formula variable as conclusion*)
    3.84 -fun convertRule vars t =
    3.85 +fun convertRule state vars t =
    3.86    let val (P::Ps) = strip_imp_prems t
    3.87        val Var v   = strip_imp_concl t
    3.88    in  v := SOME (Const ("*False*", []));
    3.89 -      (P, map (convertPrem o skoPrem vars) Ps)
    3.90 +      (P, map (convertPrem o skoPrem state vars) Ps)
    3.91    end
    3.92    handle Bind => raise ElimBadConcl;
    3.93  
    3.94 @@ -492,9 +492,9 @@
    3.95  (*Tableau rule from elimination rule.
    3.96    Flag "upd" says that the inference updated the branch.
    3.97    Flag "dup" requests duplication of the affected formula.*)
    3.98 -fun fromRule ctxt vars rl =
    3.99 +fun fromRule (state as State {ctxt, ...}) vars rl =
   3.100    let val thy = Proof_Context.theory_of ctxt
   3.101 -      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars
   3.102 +      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule state vars
   3.103        fun tac (upd, dup,rot) i =
   3.104          emtac ctxt upd (if dup then rev_dup_elim rl else rl) i
   3.105          THEN
   3.106 @@ -516,10 +516,10 @@
   3.107  
   3.108  fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
   3.109  
   3.110 -fun convertIntrRule vars t =
   3.111 +fun convertIntrRule state vars t =
   3.112    let val Ps = strip_imp_prems t
   3.113        val P  = strip_imp_concl t
   3.114 -  in  (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps)
   3.115 +  in  (mkGoal P, map (convertIntrPrem o skoPrem state vars) Ps)
   3.116    end;
   3.117  
   3.118  (*Tableau rule from introduction rule.
   3.119 @@ -527,9 +527,9 @@
   3.120    Flag "dup" requests duplication of the affected formula.
   3.121    Since haz rules are now delayed, "dup" is always FALSE for
   3.122    introduction rules.*)
   3.123 -fun fromIntrRule ctxt vars rl =
   3.124 +fun fromIntrRule (state as State {ctxt, ...}) vars rl =
   3.125    let val thy = Proof_Context.theory_of ctxt
   3.126 -      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
   3.127 +      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule state vars
   3.128        fun tac (upd,dup,rot) i =
   3.129           rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i
   3.130           THEN
   3.131 @@ -551,16 +551,16 @@
   3.132    | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
   3.133  
   3.134  
   3.135 -fun netMkRules ctxt P vars (nps: Classical.netpair list) =
   3.136 +fun netMkRules state P vars (nps: Classical.netpair list) =
   3.137    case P of
   3.138        (Const ("*Goal*", _) $ G) =>
   3.139          let val pG = mk_Trueprop (toTerm 2 G)
   3.140              val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
   3.141 -        in  map (fromIntrRule ctxt vars o #2) (order_list intrs)  end
   3.142 +        in  map (fromIntrRule state vars o #2) (order_list intrs)  end
   3.143      | _ =>
   3.144          let val pP = mk_Trueprop (toTerm 3 P)
   3.145              val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
   3.146 -        in  map_filter (fromRule ctxt vars o #2) (order_list elims)  end;
   3.147 +        in  map_filter (fromRule state vars o #2) (order_list elims)  end;
   3.148  
   3.149  
   3.150  (*Normalize a branch--for tracing*)
   3.151 @@ -936,7 +936,7 @@
   3.152                val nbrs = length brs0
   3.153                val nxtVars = nextVars brs
   3.154                val G = norm G
   3.155 -              val rules = netMkRules ctxt G vars safeList
   3.156 +              val rules = netMkRules state G vars safeList
   3.157                (*Make a new branch, decrementing "lim" if instantiations occur*)
   3.158                fun newBr (vars',lim') prems =
   3.159                    map (fn prem =>
   3.160 @@ -1030,7 +1030,7 @@
   3.161                handle CLOSEF =>   closeFl ((br,haz)::pairs)
   3.162                  handle CLOSEF => deeper rules
   3.163                    handle NEWBRANCHES =>
   3.164 -                   (case netMkRules ctxt G vars hazList of
   3.165 +                   (case netMkRules state G vars hazList of
   3.166                         [] => (*there are no plausible haz rules*)
   3.167                               (traceMsg trace "moving formula to literals";
   3.168                                prv (tacs, brs0::trs, choices,
   3.169 @@ -1064,7 +1064,7 @@
   3.170            let exception PRV (*backtrack to precisely this recursion!*)
   3.171                val H = norm H
   3.172                val ntrl = !ntrail
   3.173 -              val rules = netMkRules ctxt H vars hazList
   3.174 +              val rules = netMkRules state H vars hazList
   3.175                (*new premises of haz rules may NOT be duplicated*)
   3.176                fun newPrem (vars,P,dup,lim') prem =
   3.177                    let val Gs' = map (fn Q => (Q,false)) prem
   3.178 @@ -1188,8 +1188,9 @@
   3.179  exception TRANS of string;
   3.180  
   3.181  (*Translation of a subgoal: Skolemize all parameters*)
   3.182 -fun fromSubgoal thy t =
   3.183 -  let val alistVar = Unsynchronized.ref []
   3.184 +fun fromSubgoal (state as State {ctxt, ...}) t =
   3.185 +  let val thy = Proof_Context.theory_of ctxt
   3.186 +      val alistVar = Unsynchronized.ref []
   3.187        and alistTVar = Unsynchronized.ref []
   3.188        fun hdvar ((ix,(v,is))::_) = v
   3.189        fun from lev t =
   3.190 @@ -1227,8 +1228,7 @@
   3.191        fun skoSubgoal i t =
   3.192            if i<npars then
   3.193                skoSubgoal (i+1)
   3.194 -                (subst_bound (Skolem (gensym "T_", getVars (!alistVar) i),
   3.195 -                              t))
   3.196 +                (subst_bound (Skolem (gensym state "T", getVars (!alistVar) i), t))
   3.197            else t
   3.198  
   3.199    in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
   3.200 @@ -1238,11 +1238,10 @@
   3.201   "start" is CPU time at start, for printing SEARCH time (also prints reconstruction time)
   3.202   "lim" is depth limit.*)
   3.203  fun raw_blast start ctxt lim st =
   3.204 -  let val thy = Proof_Context.theory_of ctxt
   3.205 -      val state = initialize ctxt
   3.206 +  let val state = initialize ctxt
   3.207        val trace = Config.get ctxt trace;
   3.208        val stats = Config.get ctxt stats;
   3.209 -      val skoprem = fromSubgoal thy (#1 (Logic.dest_implies (Thm.prop_of st)))
   3.210 +      val skoprem = fromSubgoal state (#1 (Logic.dest_implies (Thm.prop_of st)))
   3.211        val hyps  = strip_imp_prems skoprem
   3.212        and concl = strip_imp_concl skoprem
   3.213        fun cont (tacs,_,choices) =
   3.214 @@ -1251,8 +1250,6 @@
   3.215            case Seq.pull(EVERY' (rev tacs) 1 st) of
   3.216                NONE => (writeln ("PROOF FAILED for depth " ^
   3.217                                  string_of_int lim);
   3.218 -                       if trace then error "************************\n"
   3.219 -                       else ();
   3.220                         backtrack trace choices)
   3.221              | cell => (if (trace orelse stats)
   3.222                         then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
   3.223 @@ -1261,6 +1258,7 @@
   3.224            end
   3.225    in
   3.226      prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
   3.227 +    |> Seq.maps Thm.flexflex_rule
   3.228    end
   3.229    handle PROVE => Seq.empty
   3.230      | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);
   3.231 @@ -1270,10 +1268,6 @@
   3.232      (Object_Logic.atomize_prems_tac 1 THEN
   3.233        raw_blast (Timing.start ()) ctxt lim) i st;
   3.234  
   3.235 -
   3.236 -val (depth_limit, setup_depth_limit) =
   3.237 -  Attrib.config_int @{binding blast_depth_limit} (K 20);
   3.238 -
   3.239  fun blast_tac ctxt i st =
   3.240    let
   3.241      val start = Timing.start ();
   3.242 @@ -1281,8 +1275,7 @@
   3.243    in
   3.244      SELECT_GOAL
   3.245       (Object_Logic.atomize_prems_tac 1 THEN
   3.246 -      DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1 THEN
   3.247 -      flexflex_tac) i st
   3.248 +      DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st
   3.249    end;
   3.250  
   3.251  
   3.252 @@ -1305,6 +1298,8 @@
   3.253  
   3.254  val setup =
   3.255    setup_depth_limit #>
   3.256 +  setup_trace #>
   3.257 +  setup_stats #>
   3.258    Method.setup @{binding blast}
   3.259      (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
   3.260        (fn NONE => SIMPLE_METHOD' o blast_tac
     4.1 --- a/src/Pure/Isar/attrib.ML	Fri Jun 10 12:01:15 2011 +0200
     4.2 +++ b/src/Pure/Isar/attrib.ML	Fri Jun 10 15:03:29 2011 +0200
     4.3 @@ -420,7 +420,7 @@
     4.4  
     4.5  val _ = Context.>> (Context.map_theory
     4.6   (register_config Ast.trace_raw #>
     4.7 -  register_config Ast.stat_raw #>
     4.8 +  register_config Ast.stats_raw #>
     4.9    register_config Syntax.positions_raw #>
    4.10    register_config Printer.show_brackets_raw #>
    4.11    register_config Printer.show_sorts_raw #>
     5.1 --- a/src/Pure/Syntax/ast.ML	Fri Jun 10 12:01:15 2011 +0200
     5.2 +++ b/src/Pure/Syntax/ast.ML	Fri Jun 10 15:03:29 2011 +0200
     5.3 @@ -23,8 +23,8 @@
     5.4    val unfold_ast_p: string -> ast -> ast list * ast
     5.5    val trace_raw: Config.raw
     5.6    val trace: bool Config.T
     5.7 -  val stat_raw: Config.raw
     5.8 -  val stat: bool Config.T
     5.9 +  val stats_raw: Config.raw
    5.10 +  val stats: bool Config.T
    5.11    val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
    5.12  end;
    5.13  
    5.14 @@ -167,8 +167,8 @@
    5.15  val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
    5.16  val trace = Config.bool trace_raw;
    5.17  
    5.18 -val stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
    5.19 -val stat = Config.bool stat_raw;
    5.20 +val stats_raw = Config.declare "syntax_ast_stats" (fn _ => Config.Bool false);
    5.21 +val stats = Config.bool stats_raw;
    5.22  
    5.23  fun message head body =
    5.24    Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
    5.25 @@ -177,7 +177,7 @@
    5.26  fun normalize ctxt get_rules pre_ast =
    5.27    let
    5.28      val trace = Config.get ctxt trace;
    5.29 -    val stat = Config.get ctxt stat;
    5.30 +    val stats = Config.get ctxt stats;
    5.31  
    5.32      val passes = Unsynchronized.ref 0;
    5.33      val failed_matches = Unsynchronized.ref 0;
    5.34 @@ -239,7 +239,7 @@
    5.35      val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else ();
    5.36      val post_ast = normal pre_ast;
    5.37      val _ =
    5.38 -      if trace orelse stat then
    5.39 +      if trace orelse stats then
    5.40          tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^
    5.41            string_of_int (! passes) ^ " passes, " ^
    5.42            string_of_int (! changes) ^ " changes, " ^