# HG changeset patch # User wenzelm # Date 1303846021 -7200 # Node ID 52fa26b6c524c1a399a7c7058b1565224548a208 # Parent d0bc1268ef09113f42560f657a9bc2dfa4200ad5 simplified Blast setup; diff -r d0bc1268ef09 -r 52fa26b6c524 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Tue Apr 26 21:05:52 2011 +0200 +++ b/src/FOL/FOL.thy Tue Apr 26 21:27:01 2011 +0200 @@ -174,18 +174,13 @@ ML {* structure Blast = Blast ( + structure Classical = Cla val thy = @{theory} - type claset = Cla.claset val equality_name = @{const_name eq} val not_name = @{const_name Not} val notE = @{thm notE} val ccontr = @{thm ccontr} - val contr_tac = Cla.contr_tac - val dup_intr = Cla.dup_intr val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac - val rep_cs = Cla.rep_cs - val cla_modifiers = Cla.cla_modifiers - val cla_meth' = Cla.cla_meth' ); val blast_tac = Blast.blast_tac; *} diff -r d0bc1268ef09 -r 52fa26b6c524 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Apr 26 21:05:52 2011 +0200 +++ b/src/HOL/HOL.thy Tue Apr 26 21:27:01 2011 +0200 @@ -927,22 +927,17 @@ done ML {* -structure Blast = Blast -( - val thy = @{theory} - type claset = Classical.claset - val equality_name = @{const_name HOL.eq} - val not_name = @{const_name Not} - val notE = @{thm notE} - val ccontr = @{thm ccontr} - val contr_tac = Classical.contr_tac - val dup_intr = Classical.dup_intr - val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac - val rep_cs = Classical.rep_cs - val cla_modifiers = Classical.cla_modifiers - val cla_meth' = Classical.cla_meth' -); -val blast_tac = Blast.blast_tac; + structure Blast = Blast + ( + structure Classical = Classical + val thy = @{theory} + val equality_name = @{const_name HOL.eq} + val not_name = @{const_name Not} + val notE = @{thm notE} + val ccontr = @{thm ccontr} + val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac + ); + val blast_tac = Blast.blast_tac; *} setup Blast.setup diff -r d0bc1268ef09 -r 52fa26b6c524 src/Provers/blast.ML --- a/src/Provers/blast.ML Tue Apr 26 21:05:52 2011 +0200 +++ b/src/Provers/blast.ML Tue Apr 26 21:27:01 2011 +0200 @@ -40,24 +40,13 @@ signature BLAST_DATA = sig + structure Classical: CLASSICAL val thy: theory - type claset val equality_name: string val not_name: string - val notE : thm (* [| ~P; P |] ==> R *) - val ccontr : thm - val contr_tac : int -> tactic - val dup_intr : thm -> thm - val hyp_subst_tac : bool -> int -> tactic - val rep_cs : (* dependent on classical.ML *) - claset -> {safeIs: thm list, safeEs: thm list, - hazIs: thm list, hazEs: thm list, - swrappers: (string * wrapper) list, - uwrappers: (string * wrapper) list, - safe0_netpair: netpair, safep_netpair: netpair, - haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair} - val cla_modifiers: Method.modifier parser list - val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method + val notE: thm (* [| ~P; P |] ==> R *) + val ccontr: thm + val hyp_subst_tac: bool -> int -> tactic end; signature BLAST = @@ -72,31 +61,31 @@ | Bound of int | Abs of string*term | $ of term*term; - type branch - val depth_tac : claset -> int -> int -> tactic - val depth_limit : int Config.T - val blast_tac : claset -> int -> tactic - val setup : theory -> theory + val depth_tac: claset -> int -> int -> tactic + val depth_limit: int Config.T + val blast_tac: claset -> int -> tactic + val setup: theory -> theory (*debugging tools*) - val stats : bool Unsynchronized.ref - val trace : bool Unsynchronized.ref - val fullTrace : branch list list Unsynchronized.ref - 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 : theory -> string -> term - val tryInThy : theory -> claset -> int -> string -> - (int->tactic) list * branch list list * (int*int*exn) list - val normBr : branch -> branch + type branch + val stats: bool Unsynchronized.ref + val trace: bool Unsynchronized.ref + val fullTrace: branch list list Unsynchronized.ref + 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: theory -> string -> term + val tryInThy: theory -> claset -> int -> string -> + (int -> tactic) list * branch list list * (int * int * exn) list + val normBr: branch -> branch end; - -functor Blast(Data: BLAST_DATA) : BLAST = +functor Blast(Data: BLAST_DATA): BLAST = struct -type claset = Data.claset; +structure Classical = Data.Classical; +type claset = Classical.claset; val trace = Unsynchronized.ref false and stats = Unsynchronized.ref false; (*for runtime and search statistics*) @@ -541,7 +530,7 @@ fun fromIntrRule thy vars rl = let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars fun tac (upd,dup,rot) i = - rmtac upd (if dup then Data.dup_intr rl else rl) i + rmtac upd (if dup then Classical.dup_intr rl else rl) i THEN rot_subgoals_tac (rot, #2 trl) i in (trl, tac) end; @@ -928,7 +917,7 @@ *) fun prove (state, start, cs, brs, cont) = let val State {thy, ntrail, nclosed, ntried, ...} = state; - val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs + val {safe0_netpair, safep_netpair, haz_netpair, ...} = Classical.rep_cs cs val safeList = [safe0_netpair, safep_netpair] and hazList = [haz_netpair] fun prv (tacs, trs, choices, []) = @@ -1314,9 +1303,9 @@ val setup = setup_depth_limit #> Method.setup @{binding blast} - (Scan.lift (Scan.option Parse.nat) --| Method.sections Data.cla_modifiers >> - (fn NONE => Data.cla_meth' blast_tac - | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim))) + (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >> + (fn NONE => Classical.cla_meth' blast_tac + | SOME lim => Classical.cla_meth' (fn cs => depth_tac cs lim))) "classical tableau prover"; end;