src/Provers/blast.ML
changeset 43349 46b4f57fb034
parent 43348 3e153e719039
child 46715 6236ca7b32a7
     1.1 --- a/src/Provers/blast.ML	Fri Jun 10 12:51:29 2011 +0200
     1.2 +++ b/src/Provers/blast.ML	Fri Jun 10 13:32:51 2011 +0200
     1.3 @@ -59,22 +59,15 @@
     1.4      | $  of term*term;
     1.5    val depth_tac: Proof.context -> int -> int -> tactic
     1.6    val depth_limit: int Config.T
     1.7 +  val trace: bool Config.T
     1.8 +  val stats: bool Config.T
     1.9    val blast_tac: Proof.context -> int -> tactic
    1.10    val setup: theory -> theory
    1.11    (*debugging tools*)
    1.12    type branch
    1.13 -  val trace: bool Config.T
    1.14 -  val stats: bool Config.T
    1.15 -  val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term
    1.16 -  val fromTerm: theory -> Term.term -> term
    1.17 -  val fromSubgoal: theory -> Term.term -> term
    1.18 -  val instVars: term -> (unit -> unit)
    1.19 -  val toTerm: int -> term -> Term.term
    1.20 -  val readGoal: Proof.context -> string -> term
    1.21    val tryIt: Proof.context -> int -> string ->
    1.22      {fullTrace: branch list list,
    1.23        result: ((int -> tactic) list * branch list list * (int * int * exn) list)}
    1.24 -  val normBr: branch -> branch
    1.25  end;
    1.26  
    1.27  functor Blast(Data: BLAST_DATA): BLAST =
    1.28 @@ -111,6 +104,7 @@
    1.29  
    1.30  datatype state = State of
    1.31   {ctxt: Proof.context,
    1.32 +  names: Name.context Unsynchronized.ref,
    1.33    fullTrace: branch list list Unsynchronized.ref,
    1.34    trail: term option Unsynchronized.ref list Unsynchronized.ref,
    1.35    ntrail: int Unsynchronized.ref,
    1.36 @@ -129,6 +123,7 @@
    1.37    in
    1.38      State
    1.39       {ctxt = ctxt,
    1.40 +      names = Unsynchronized.ref (Variable.names_of ctxt),
    1.41        fullTrace = Unsynchronized.ref [],
    1.42        trail = Unsynchronized.ref [],
    1.43        ntrail = Unsynchronized.ref 0,
    1.44 @@ -136,6 +131,8 @@
    1.45        ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*)
    1.46    end;
    1.47  
    1.48 +fun gensym (State {names, ...}) x =
    1.49 +  Unsynchronized.change_result names (Name.variant x);
    1.50  
    1.51  
    1.52  (** Basic syntactic operations **)
    1.53 @@ -446,19 +443,19 @@
    1.54            else P :: delete_concl Ps
    1.55        | _ => P :: delete_concl Ps);
    1.56  
    1.57 -fun skoPrem vars (Const ("all", _) $ Abs (_, P)) =
    1.58 -        skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
    1.59 -  | skoPrem vars P = P;
    1.60 +fun skoPrem state vars (Const ("all", _) $ Abs (_, P)) =
    1.61 +        skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P))
    1.62 +  | skoPrem _ _ P = P;
    1.63  
    1.64  fun convertPrem t =
    1.65      delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
    1.66  
    1.67  (*Expects elimination rules to have a formula variable as conclusion*)
    1.68 -fun convertRule vars t =
    1.69 +fun convertRule state vars t =
    1.70    let val (P::Ps) = strip_imp_prems t
    1.71        val Var v   = strip_imp_concl t
    1.72    in  v := SOME (Const ("*False*", []));
    1.73 -      (P, map (convertPrem o skoPrem vars) Ps)
    1.74 +      (P, map (convertPrem o skoPrem state vars) Ps)
    1.75    end
    1.76    handle Bind => raise ElimBadConcl;
    1.77  
    1.78 @@ -495,9 +492,9 @@
    1.79  (*Tableau rule from elimination rule.
    1.80    Flag "upd" says that the inference updated the branch.
    1.81    Flag "dup" requests duplication of the affected formula.*)
    1.82 -fun fromRule ctxt vars rl =
    1.83 +fun fromRule (state as State {ctxt, ...}) vars rl =
    1.84    let val thy = Proof_Context.theory_of ctxt
    1.85 -      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars
    1.86 +      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule state vars
    1.87        fun tac (upd, dup,rot) i =
    1.88          emtac ctxt upd (if dup then rev_dup_elim rl else rl) i
    1.89          THEN
    1.90 @@ -519,10 +516,10 @@
    1.91  
    1.92  fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
    1.93  
    1.94 -fun convertIntrRule vars t =
    1.95 +fun convertIntrRule state vars t =
    1.96    let val Ps = strip_imp_prems t
    1.97        val P  = strip_imp_concl t
    1.98 -  in  (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps)
    1.99 +  in  (mkGoal P, map (convertIntrPrem o skoPrem state vars) Ps)
   1.100    end;
   1.101  
   1.102  (*Tableau rule from introduction rule.
   1.103 @@ -530,9 +527,9 @@
   1.104    Flag "dup" requests duplication of the affected formula.
   1.105    Since haz rules are now delayed, "dup" is always FALSE for
   1.106    introduction rules.*)
   1.107 -fun fromIntrRule ctxt vars rl =
   1.108 +fun fromIntrRule (state as State {ctxt, ...}) vars rl =
   1.109    let val thy = Proof_Context.theory_of ctxt
   1.110 -      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
   1.111 +      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule state vars
   1.112        fun tac (upd,dup,rot) i =
   1.113           rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i
   1.114           THEN
   1.115 @@ -554,16 +551,16 @@
   1.116    | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
   1.117  
   1.118  
   1.119 -fun netMkRules ctxt P vars (nps: Classical.netpair list) =
   1.120 +fun netMkRules state P vars (nps: Classical.netpair list) =
   1.121    case P of
   1.122        (Const ("*Goal*", _) $ G) =>
   1.123          let val pG = mk_Trueprop (toTerm 2 G)
   1.124              val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
   1.125 -        in  map (fromIntrRule ctxt vars o #2) (order_list intrs)  end
   1.126 +        in  map (fromIntrRule state vars o #2) (order_list intrs)  end
   1.127      | _ =>
   1.128          let val pP = mk_Trueprop (toTerm 3 P)
   1.129              val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
   1.130 -        in  map_filter (fromRule ctxt vars o #2) (order_list elims)  end;
   1.131 +        in  map_filter (fromRule state vars o #2) (order_list elims)  end;
   1.132  
   1.133  
   1.134  (*Normalize a branch--for tracing*)
   1.135 @@ -939,7 +936,7 @@
   1.136                val nbrs = length brs0
   1.137                val nxtVars = nextVars brs
   1.138                val G = norm G
   1.139 -              val rules = netMkRules ctxt G vars safeList
   1.140 +              val rules = netMkRules state G vars safeList
   1.141                (*Make a new branch, decrementing "lim" if instantiations occur*)
   1.142                fun newBr (vars',lim') prems =
   1.143                    map (fn prem =>
   1.144 @@ -1033,7 +1030,7 @@
   1.145                handle CLOSEF =>   closeFl ((br,haz)::pairs)
   1.146                  handle CLOSEF => deeper rules
   1.147                    handle NEWBRANCHES =>
   1.148 -                   (case netMkRules ctxt G vars hazList of
   1.149 +                   (case netMkRules state G vars hazList of
   1.150                         [] => (*there are no plausible haz rules*)
   1.151                               (traceMsg trace "moving formula to literals";
   1.152                                prv (tacs, brs0::trs, choices,
   1.153 @@ -1067,7 +1064,7 @@
   1.154            let exception PRV (*backtrack to precisely this recursion!*)
   1.155                val H = norm H
   1.156                val ntrl = !ntrail
   1.157 -              val rules = netMkRules ctxt H vars hazList
   1.158 +              val rules = netMkRules state H vars hazList
   1.159                (*new premises of haz rules may NOT be duplicated*)
   1.160                fun newPrem (vars,P,dup,lim') prem =
   1.161                    let val Gs' = map (fn Q => (Q,false)) prem
   1.162 @@ -1191,8 +1188,9 @@
   1.163  exception TRANS of string;
   1.164  
   1.165  (*Translation of a subgoal: Skolemize all parameters*)
   1.166 -fun fromSubgoal thy t =
   1.167 -  let val alistVar = Unsynchronized.ref []
   1.168 +fun fromSubgoal (state as State {ctxt, ...}) t =
   1.169 +  let val thy = Proof_Context.theory_of ctxt
   1.170 +      val alistVar = Unsynchronized.ref []
   1.171        and alistTVar = Unsynchronized.ref []
   1.172        fun hdvar ((ix,(v,is))::_) = v
   1.173        fun from lev t =
   1.174 @@ -1230,8 +1228,7 @@
   1.175        fun skoSubgoal i t =
   1.176            if i<npars then
   1.177                skoSubgoal (i+1)
   1.178 -                (subst_bound (Skolem (gensym "T_", getVars (!alistVar) i),
   1.179 -                              t))
   1.180 +                (subst_bound (Skolem (gensym state "T", getVars (!alistVar) i), t))
   1.181            else t
   1.182  
   1.183    in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
   1.184 @@ -1241,11 +1238,10 @@
   1.185   "start" is CPU time at start, for printing SEARCH time (also prints reconstruction time)
   1.186   "lim" is depth limit.*)
   1.187  fun raw_blast start ctxt lim st =
   1.188 -  let val thy = Proof_Context.theory_of ctxt
   1.189 -      val state = initialize ctxt
   1.190 +  let val state = initialize ctxt
   1.191        val trace = Config.get ctxt trace;
   1.192        val stats = Config.get ctxt stats;
   1.193 -      val skoprem = fromSubgoal thy (#1 (Logic.dest_implies (Thm.prop_of st)))
   1.194 +      val skoprem = fromSubgoal state (#1 (Logic.dest_implies (Thm.prop_of st)))
   1.195        val hyps  = strip_imp_prems skoprem
   1.196        and concl = strip_imp_concl skoprem
   1.197        fun cont (tacs,_,choices) =