Tidying; more debugging information. New reference unwanted_types.
authorpaulson
Wed Jan 31 14:03:31 2007 +0100 (2007-01-31)
changeset 22217a5d983f7113f
parent 22216 c3f5aa951a68
child 22218 30a8890d2967
Tidying; more debugging information. New reference unwanted_types.
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Jan 30 13:17:02 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jan 31 14:03:31 2007 +0100
     1.3 @@ -472,10 +472,8 @@
     1.4    end;
     1.5  
     1.6  fun make_banned_test xs =
     1.7 -  let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
     1.8 -                                (6000, HASH_STRING)
     1.9 -      fun banned s =
    1.10 -            isSome (Polyhash.peek ht s) orelse is_package_def s
    1.11 +  let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) (6000, HASH_STRING)
    1.12 +      fun banned s = isSome (Polyhash.peek ht s) orelse is_package_def s
    1.13    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
    1.14        banned
    1.15    end;
    1.16 @@ -696,14 +694,19 @@
    1.17          | var_tycon _ = false
    1.18    in  exists var_tycon o term_vars  end;
    1.19  
    1.20 +(*Clauses are forbidden to contain variables of these types. The typical reason is that
    1.21 +  they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
    1.22 +  The resulting clause will have no type constraint, yielding false proofs. Even "bool"
    1.23 +  leads to many unsound proofs, though (obviously) only for higher-order problems.*)
    1.24 +val unwanted_types = ref ["Product_Type.unit","bool"];
    1.25 +
    1.26  fun unwanted t =
    1.27 -    is_taut t orelse has_typed_var ["Product_Type.unit","bool"] t orelse
    1.28 +    is_taut t orelse has_typed_var (!unwanted_types) t orelse
    1.29      forall too_general_equality (dest_disj t);
    1.30  
    1.31  (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
    1.32    likely to lead to unsound proofs.*)
    1.33 -fun remove_unwanted_clauses cls =
    1.34 -  filter (not o unwanted o prop_of o fst) cls;
    1.35 +fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
    1.36  
    1.37  fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
    1.38      if is_fol_logic logic
    1.39 @@ -851,8 +854,13 @@
    1.40        fun write_all [] [] _ = []
    1.41          | write_all (ccls::ccls_list) (axcls::axcls_list) k =
    1.42              let val fname = probfile k
    1.43 +                val _ = Output.debug (fn () => "About to write file " ^ fname)
    1.44                  val axcls = make_unique axcls
    1.45 +                val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)")
    1.46 +                val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
    1.47                  val ccls = subtract_cls ccls axcls
    1.48 +                val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)")
    1.49 +                val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
    1.50                  val ccltms = map prop_of ccls
    1.51                  and axtms = map (prop_of o #1) axcls
    1.52                  val subs = tfree_classes_of_terms ccltms