src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 37566 9ca40dff25bd
parent 37515 ef3742657bc6
child 37570 de5feddaa95c
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 25 12:15:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Jun 25 15:01:35 2010 +0200
     1.3 @@ -27,15 +27,23 @@
     1.4    datatype hol_clause =
     1.5      HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
     1.6                    literals: literal list, ctypes_sorts: typ list}
     1.7 +  exception TRIVIAL of unit
     1.8  
     1.9    val type_of_combterm : combterm -> combtyp
    1.10    val strip_combterm_comb : combterm -> combterm * combterm list
    1.11    val literals_of_term : theory -> term -> literal list * typ list
    1.12    val conceal_skolem_somes :
    1.13      int -> (string * term) list -> term -> (string * term) list * term
    1.14 -  exception TRIVIAL of unit
    1.15 -  val make_conjecture_clauses : theory -> thm list -> hol_clause list
    1.16 -  val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
    1.17 +  val is_quasi_fol_theorem : theory -> thm -> bool
    1.18 +  val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
    1.19 +  val tfree_classes_of_terms : term list -> string list
    1.20 +  val tvar_classes_of_terms : term list -> string list
    1.21 +  val type_consts_of_terms : theory -> term list -> string list
    1.22 +  val prepare_clauses :
    1.23 +    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
    1.24 +    -> string vector
    1.25 +       * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
    1.26 +          * classrel_clause list * arity_clause list)
    1.27  end
    1.28  
    1.29  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    1.30 @@ -192,6 +200,9 @@
    1.31    else
    1.32      (skolem_somes, t)
    1.33  
    1.34 +fun is_quasi_fol_theorem thy =
    1.35 +  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
    1.36 +
    1.37  (* Trivial problem, which resolution cannot handle (empty clause) *)
    1.38  exception TRIVIAL of unit
    1.39  
    1.40 @@ -228,4 +239,116 @@
    1.41          in cls :: aux (n + 1) skolem_somes ths end
    1.42    in aux 0 [] end
    1.43  
    1.44 +(** Helper clauses **)
    1.45 +
    1.46 +fun count_combterm (CombConst ((c, _), _, _)) =
    1.47 +    Symtab.map_entry c (Integer.add 1)
    1.48 +  | count_combterm (CombVar _) = I
    1.49 +  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
    1.50 +fun count_literal (Literal (_, t)) = count_combterm t
    1.51 +fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
    1.52 +
    1.53 +fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
    1.54 +fun cnf_helper_thms thy raw =
    1.55 +  map (`Thm.get_name_hint)
    1.56 +  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
    1.57 +
    1.58 +val optional_helpers =
    1.59 +  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
    1.60 +   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
    1.61 +   (["c_COMBS"], (false, @{thms COMBS_def}))]
    1.62 +val optional_typed_helpers =
    1.63 +  [(["c_True", "c_False"], (true, @{thms True_or_False})),
    1.64 +   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
    1.65 +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
    1.66 +
    1.67 +val init_counters =
    1.68 +  Symtab.make (maps (maps (map (rpair 0) o fst))
    1.69 +                    [optional_helpers, optional_typed_helpers])
    1.70 +
    1.71 +fun get_helper_clauses thy is_FO full_types conjectures axcls =
    1.72 +  let
    1.73 +    val axclauses = map snd (make_axiom_clauses thy axcls)
    1.74 +    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
    1.75 +    fun is_needed c = the (Symtab.lookup ct c) > 0
    1.76 +    val cnfs =
    1.77 +      (optional_helpers
    1.78 +       |> full_types ? append optional_typed_helpers
    1.79 +       |> maps (fn (ss, (raw, ths)) =>
    1.80 +                   if exists is_needed ss then cnf_helper_thms thy raw ths
    1.81 +                   else []))
    1.82 +      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
    1.83 +  in map snd (make_axiom_clauses thy cnfs) end
    1.84 +
    1.85 +fun make_clause_table xs =
    1.86 +  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
    1.87 +
    1.88 +
    1.89 +(***************************************************************)
    1.90 +(* Type Classes Present in the Axiom or Conjecture Clauses     *)
    1.91 +(***************************************************************)
    1.92 +
    1.93 +fun set_insert (x, s) = Symtab.update (x, ()) s
    1.94 +
    1.95 +fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
    1.96 +
    1.97 +(*Remove this trivial type class*)
    1.98 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
    1.99 +
   1.100 +fun tfree_classes_of_terms ts =
   1.101 +  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   1.102 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   1.103 +
   1.104 +fun tvar_classes_of_terms ts =
   1.105 +  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   1.106 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   1.107 +
   1.108 +(*fold type constructors*)
   1.109 +fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   1.110 +  | fold_type_consts _ _ x = x;
   1.111 +
   1.112 +(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   1.113 +fun add_type_consts_in_term thy =
   1.114 +  let
   1.115 +    val const_typargs = Sign.const_typargs thy
   1.116 +    fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
   1.117 +      | aux (Abs (_, _, u)) = aux u
   1.118 +      | aux (Const (@{const_name skolem_id}, _) $ _) = I
   1.119 +      | aux (t $ u) = aux t #> aux u
   1.120 +      | aux _ = I
   1.121 +  in aux end
   1.122 +
   1.123 +fun type_consts_of_terms thy ts =
   1.124 +  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   1.125 +
   1.126 +(* Remove existing axiom clauses from the conjecture clauses, as this can
   1.127 +   dramatically boost an ATP's performance (for some reason). *)
   1.128 +fun subtract_cls ax_clauses =
   1.129 +  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
   1.130 +
   1.131 +(* prepare for passing to writer,
   1.132 +   create additional clauses based on the information from extra_cls *)
   1.133 +fun prepare_clauses full_types goal_cls axcls extra_cls thy =
   1.134 +  let
   1.135 +    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
   1.136 +    val ccls = subtract_cls extra_cls goal_cls
   1.137 +    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   1.138 +    val ccltms = map prop_of ccls
   1.139 +    and axtms = map (prop_of o #1) extra_cls
   1.140 +    val subs = tfree_classes_of_terms ccltms
   1.141 +    and supers = tvar_classes_of_terms axtms
   1.142 +    and tycons = type_consts_of_terms thy (ccltms @ axtms)
   1.143 +    (*TFrees in conjecture clauses; TVars in axiom clauses*)
   1.144 +    val conjectures = make_conjecture_clauses thy ccls
   1.145 +    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
   1.146 +    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
   1.147 +    val helper_clauses =
   1.148 +      get_helper_clauses thy is_FO full_types conjectures extra_cls
   1.149 +    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   1.150 +    val classrel_clauses = make_classrel_clauses thy subs supers'
   1.151 +  in
   1.152 +    (Vector.fromList clnames,
   1.153 +      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   1.154 +  end
   1.155 +
   1.156  end;