# HG changeset patch # User paulson # Date 1121165386 -7200 # Node ID 515b6020cf5d532ef88842bb4ff02bfeb17c40b9 # Parent 33c4d8fe6f78af04538e884c0575f731823e33fc experimental code to reduce the amount of type information in blast diff -r 33c4d8fe6f78 -r 515b6020cf5d src/FOL/blastdata.ML --- a/src/FOL/blastdata.ML Tue Jul 12 12:49:00 2005 +0200 +++ b/src/FOL/blastdata.ML Tue Jul 12 12:49:46 2005 +0200 @@ -3,6 +3,7 @@ structure Blast_Data = struct type claset = Cla.claset + val is_hol = false val notE = notE val ccontr = ccontr val contr_tac = Cla.contr_tac diff -r 33c4d8fe6f78 -r 515b6020cf5d src/HOL/blastdata.ML --- a/src/HOL/blastdata.ML Tue Jul 12 12:49:00 2005 +0200 +++ b/src/HOL/blastdata.ML Tue Jul 12 12:49:46 2005 +0200 @@ -16,6 +16,7 @@ structure Blast_Data = struct type claset = Classical.claset + val is_hol = true val notE = notE val ccontr = ccontr val contr_tac = Classical.contr_tac diff -r 33c4d8fe6f78 -r 515b6020cf5d src/Provers/blast.ML --- a/src/Provers/blast.ML Tue Jul 12 12:49:00 2005 +0200 +++ b/src/Provers/blast.ML Tue Jul 12 12:49:46 2005 +0200 @@ -48,6 +48,7 @@ sig type claset val notE : thm (* [| ~P; P |] ==> R *) + val is_hol : bool (*Is this HOL or FOL/ZF?*) val ccontr : thm val contr_tac : int -> tactic val dup_intr : thm -> thm @@ -130,20 +131,17 @@ fun dest_Var (Var x) = x; - fun rand (f$x) = x; (* maps (f, [t1,...,tn]) to f(t1,...,tn) *) val list_comb : term * term list -> term = Library.foldl (op $); - (* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*) fun strip_comb u : term * term list = let fun stripc (f$t, ts) = stripc (f, t::ts) | stripc x = x in stripc(u,[]) end; - (* maps f(t1,...,tn) to f , which is never a combination *) fun head_of (f$t) = head_of f | head_of u = u; @@ -158,7 +156,8 @@ fun isGoal (Const"*Goal*" $ _) = true | isGoal _ = false; -val Trueprop = Term.Const("Trueprop", Type("o",[])-->propT); +val boolT = if Data.is_hol then "bool" else "o"; +val Trueprop = Term.Const("Trueprop", Type(boolT,[])-->propT); fun mk_tprop P = Term.$ (Trueprop, P); fun isTrueprop (Term.Const("Trueprop",_)) = true @@ -169,8 +168,7 @@ (*alist is a map from TVar names to Vars. We need to unify the TVars faithfully in order to track overloading*) -fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, - map (fromType alist) Ts) +fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, map (fromType alist) Ts) | fromType alist (Term.TFree(a,_)) = Free a | fromType alist (Term.TVar (ixn,_)) = (case (assoc_string_int(!alist,ixn)) of @@ -179,21 +177,25 @@ end | SOME v => v) -(*Monomorphic constants used in blast, plus binary propositional connectives.*) -val standard_consts = - ["Not", "op &", "op |", "op -->", "op <->", - "*Goal*", "*False*", "==>", "all", "Trueprop"]; +(*Definitions of the theory in which blast is initialized.*) +val curr_defs = ref Defs.empty; -val standard_const_table = Symtab.make (map (rpair()) standard_consts) +(*Types aren't needed if the constant has at most one definition and is monomorphic*) +fun no_types_needed s = + (case Defs.overloading_info (!curr_defs) s of + NONE => true + | SOME (T,defs,_) => length defs <= 1 andalso null (typ_tvars T)) + handle Option => (warning ("Defs.overloading_info failed for " ^ s); false); (*Convert a Term.Const to a Blast.Const or Blast.TConst, converting its type to a Blast.term in the latter case. - Const is used for a small number of built-in operators that are - known to be monomorphic, which promotes efficiency. *) + For efficiency, Const is used for FOL and for the logical constants. + We can't use it for all non-overloaded operators because some preservation + of type information is necessary to prevent PROOF FAILED elsewhere.*) fun fromConst alist (a,T) = - case Symtab.lookup(standard_const_table, a) of - NONE => TConst(a, fromType alist T) - | SOME() => Const(a) + if not Data.is_hol orelse a mem_string ["All","Ex","all"] orelse no_types_needed a + then Const a + else TConst(a, fromType alist T); (*Tests whether 2 terms are alpha-convertible; chases instantiations*) @@ -377,8 +379,8 @@ end; -(*Convert from "real" terms to prototerms; eta-contract - Code is duplicated with fromSubgoal. Correct this?*) +(*Convert from "real" terms to prototerms; eta-contract. + Code is similar to fromSubgoal.*) fun fromTerm t = let val alistVar = ref [] and alistTVar = ref [] @@ -597,9 +599,7 @@ (*Display top-level overloading if any*) fun topType (TConst(a,t)) = SOME (showType t) | topType (Abs(a,t)) = topType t - | topType (f $ u) = (case topType f of - NONE => topType u - | some => some) + | topType (f $ u) = (case topType f of NONE => topType u | some => some) | topType _ = NONE; @@ -1247,9 +1247,9 @@ in skoSubgoal 0 (from 0 (discard_foralls t)) end; -fun initialize() = +fun initialize thy = (fullTrace:=[]; trail := []; ntrail := 0; - nclosed := 0; ntried := 1); + nclosed := 0; ntried := 1; curr_defs := Theory.defs_of thy); (*Tactic using tableau engine and proof reconstruction. @@ -1257,8 +1257,7 @@ (also prints reconstruction time) "lim" is depth limit.*) fun timing_depth_tac start cs lim i st0 = - (initialize(); - let val st = ObjectLogic.atomize_goal i st0; + let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0); val {sign,...} = rep_thm st val skoprem = fromSubgoal (List.nth(prems_of st, i-1)) val hyps = strip_imp_prems skoprem @@ -1269,7 +1268,7 @@ case Seq.pull(EVERY' (rev tacs) i st) of NONE => (writeln ("PROOF FAILED for depth " ^ Int.toString lim); - if !trace then writeln "************************\n" + if !trace then error "************************\n" else (); backtrack choices) | cell => (if (!trace orelse !stats) @@ -1279,7 +1278,7 @@ end in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end - handle PROVE => Seq.empty); + handle PROVE => Seq.empty; (*Public version with fixed depth*) fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st; @@ -1301,16 +1300,16 @@ (*Translate subgoal i from a proof state*) fun trygl cs lim i = - (initialize(); - let val st = topthm() - val {sign,...} = rep_thm st - val skoprem = fromSubgoal (List.nth(prems_of st, i-1)) - val hyps = strip_imp_prems skoprem - and concl = strip_imp_concl skoprem - in timeap prove (sign, startTiming(), cs, - [initBranch (mkGoal concl :: hyps, lim)], I) - end - handle Subscript => error("There is no subgoal " ^ Int.toString i)); + let val st = topthm() + val {sign,...} = rep_thm st + val skoprem = (initialize (theory_of_thm st); + fromSubgoal (List.nth(prems_of st, i-1))) + val hyps = strip_imp_prems skoprem + and concl = strip_imp_concl skoprem + in timeap prove (sign, startTiming(), cs, + [initBranch (mkGoal concl :: hyps, lim)], I) + end + handle Subscript => error("There is no subgoal " ^ Int.toString i); fun Trygl lim i = trygl (Data.claset()) lim i; @@ -1319,7 +1318,7 @@ term_of |> fromTerm |> rand |> mkGoal; fun tryInThy thy lim s = - (initialize(); + (initialize thy; timeap prove (Theory.sign_of thy, startTiming(), Data.claset(),