src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
author blanchet
Fri Jun 25 15:01:35 2010 +0200 (2010-06-25 ago)
changeset 37566 9ca40dff25bd
parent 37515 ef3742657bc6
child 37570 de5feddaa95c
permissions -rw-r--r--
move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
since it has nothing to do with filtering
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
     2     Author:     Jia Meng, NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 FOL clauses translated from HOL formulas.
     6 *)
     7 
     8 signature SLEDGEHAMMER_HOL_CLAUSE =
     9 sig
    10   type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
    11   type name = Sledgehammer_FOL_Clause.name
    12   type name_pool = Sledgehammer_FOL_Clause.name_pool
    13   type kind = Sledgehammer_FOL_Clause.kind
    14   type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
    15   type arity_clause = Sledgehammer_FOL_Clause.arity_clause
    16   type polarity = bool
    17 
    18   datatype combtyp =
    19     TyVar of name |
    20     TyFree of name |
    21     TyConstr of name * combtyp list
    22   datatype combterm =
    23     CombConst of name * combtyp * combtyp list (* Const and Free *) |
    24     CombVar of name * combtyp |
    25     CombApp of combterm * combterm
    26   datatype literal = Literal of polarity * combterm
    27   datatype hol_clause =
    28     HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    29                   literals: literal list, ctypes_sorts: typ list}
    30   exception TRIVIAL of unit
    31 
    32   val type_of_combterm : combterm -> combtyp
    33   val strip_combterm_comb : combterm -> combterm * combterm list
    34   val literals_of_term : theory -> term -> literal list * typ list
    35   val conceal_skolem_somes :
    36     int -> (string * term) list -> term -> (string * term) list * term
    37   val is_quasi_fol_theorem : theory -> thm -> bool
    38   val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
    39   val tfree_classes_of_terms : term list -> string list
    40   val tvar_classes_of_terms : term list -> string list
    41   val type_consts_of_terms : theory -> term list -> string list
    42   val prepare_clauses :
    43     bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
    44     -> string vector
    45        * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
    46           * classrel_clause list * arity_clause list)
    47 end
    48 
    49 structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    50 struct
    51 
    52 open Sledgehammer_Util
    53 open Sledgehammer_FOL_Clause
    54 open Sledgehammer_Fact_Preprocessor
    55 
    56 (******************************************************)
    57 (* data types for typed combinator expressions        *)
    58 (******************************************************)
    59 
    60 type polarity = bool
    61 
    62 datatype combtyp =
    63   TyVar of name |
    64   TyFree of name |
    65   TyConstr of name * combtyp list
    66 
    67 datatype combterm =
    68   CombConst of name * combtyp * combtyp list (* Const and Free *) |
    69   CombVar of name * combtyp |
    70   CombApp of combterm * combterm
    71 
    72 datatype literal = Literal of polarity * combterm;
    73 
    74 datatype hol_clause =
    75   HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    76                 literals: literal list, ctypes_sorts: typ list}
    77 
    78 (*********************************************************************)
    79 (* convert a clause with type Term.term to a clause with type clause *)
    80 (*********************************************************************)
    81 
    82 (*Result of a function type; no need to check that the argument type matches.*)
    83 fun result_type (TyConstr (_, [_, tp2])) = tp2
    84   | result_type _ = raise Fail "non-function type"
    85 
    86 fun type_of_combterm (CombConst (_, tp, _)) = tp
    87   | type_of_combterm (CombVar (_, tp)) = tp
    88   | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
    89 
    90 (*gets the head of a combinator application, along with the list of arguments*)
    91 fun strip_combterm_comb u =
    92     let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
    93         |   stripc  x =  x
    94     in stripc(u,[]) end
    95 
    96 fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
    97       (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
    98   | isFalse _ = false;
    99 
   100 fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
   101       (pol andalso c = "c_True") orelse
   102       (not pol andalso c = "c_False")
   103   | isTrue _ = false;
   104 
   105 fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
   106 
   107 fun type_of (Type (a, Ts)) =
   108     let val (folTypes,ts) = types_of Ts in
   109       (TyConstr (`make_fixed_type_const a, folTypes), ts)
   110     end
   111   | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
   112   | type_of (tp as TVar (x, _)) =
   113     (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
   114 and types_of Ts =
   115     let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
   116       (folTyps, union_all ts)
   117     end
   118 
   119 (* same as above, but no gathering of sort information *)
   120 fun simp_type_of (Type (a, Ts)) =
   121       TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
   122   | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
   123   | simp_type_of (TVar (x, _)) =
   124     TyVar (make_schematic_type_var x, string_of_indexname x)
   125 
   126 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   127 fun combterm_of thy (Const (c, T)) =
   128       let
   129         val (tp, ts) = type_of T
   130         val tvar_list =
   131           (if String.isPrefix skolem_theory_name c then
   132              [] |> Term.add_tvarsT T |> map TVar
   133            else
   134              (c, T) |> Sign.const_typargs thy)
   135           |> map simp_type_of
   136         val c' = CombConst (`make_fixed_const c, tp, tvar_list)
   137       in  (c',ts)  end
   138   | combterm_of _ (Free(v, T)) =
   139       let val (tp,ts) = type_of T
   140           val v' = CombConst (`make_fixed_var v, tp, [])
   141       in  (v',ts)  end
   142   | combterm_of _ (Var(v, T)) =
   143       let val (tp,ts) = type_of T
   144           val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
   145       in  (v',ts)  end
   146   | combterm_of thy (P $ Q) =
   147       let val (P', tsP) = combterm_of thy P
   148           val (Q', tsQ) = combterm_of thy Q
   149       in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   150   | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t)
   151 
   152 fun predicate_of thy ((@{const Not} $ P), polarity) =
   153     predicate_of thy (P, not polarity)
   154   | predicate_of thy (t, polarity) =
   155     (combterm_of thy (Envir.eta_contract t), polarity)
   156 
   157 fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   158     literals_of_term1 args thy P
   159   | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
   160     literals_of_term1 (literals_of_term1 args thy P) thy Q
   161   | literals_of_term1 (lits, ts) thy P =
   162     let val ((pred, ts'), pol) = predicate_of thy (P, true) in
   163       (Literal (pol, pred) :: lits, union (op =) ts ts')
   164     end
   165 val literals_of_term = literals_of_term1 ([], [])
   166 
   167 fun skolem_name i j num_T_args =
   168   skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
   169   skolem_infix ^ "g"
   170 
   171 fun conceal_skolem_somes i skolem_somes t =
   172   if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
   173     let
   174       fun aux skolem_somes
   175               (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
   176           let
   177             val (skolem_somes, s) =
   178               if i = ~1 then
   179                 (skolem_somes, @{const_name undefined})
   180               else case AList.find (op aconv) skolem_somes t of
   181                 s :: _ => (skolem_somes, s)
   182               | [] =>
   183                 let
   184                   val s = skolem_theory_name ^ "." ^
   185                           skolem_name i (length skolem_somes)
   186                                         (length (Term.add_tvarsT T []))
   187                 in ((s, t) :: skolem_somes, s) end
   188           in (skolem_somes, Const (s, T)) end
   189         | aux skolem_somes (t1 $ t2) =
   190           let
   191             val (skolem_somes, t1) = aux skolem_somes t1
   192             val (skolem_somes, t2) = aux skolem_somes t2
   193           in (skolem_somes, t1 $ t2) end
   194         | aux skolem_somes (Abs (s, T, t')) =
   195           let val (skolem_somes, t') = aux skolem_somes t' in
   196             (skolem_somes, Abs (s, T, t'))
   197           end
   198         | aux skolem_somes t = (skolem_somes, t)
   199     in aux skolem_somes t end
   200   else
   201     (skolem_somes, t)
   202 
   203 fun is_quasi_fol_theorem thy =
   204   Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
   205 
   206 (* Trivial problem, which resolution cannot handle (empty clause) *)
   207 exception TRIVIAL of unit
   208 
   209 (* making axiom and conjecture clauses *)
   210 fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
   211   let
   212     val (skolem_somes, t) =
   213       th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
   214     val (lits, ctypes_sorts) = literals_of_term thy t
   215   in
   216     if forall isFalse lits then
   217       raise TRIVIAL ()
   218     else
   219       (skolem_somes,
   220        HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
   221                   kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   222   end
   223 
   224 fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
   225   let
   226     val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
   227   in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
   228 
   229 fun make_axiom_clauses thy clauses =
   230   ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
   231 
   232 fun make_conjecture_clauses thy =
   233   let
   234     fun aux _ _ [] = []
   235       | aux n skolem_somes (th :: ths) =
   236         let
   237           val (skolem_somes, cls) =
   238             make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
   239         in cls :: aux (n + 1) skolem_somes ths end
   240   in aux 0 [] end
   241 
   242 (** Helper clauses **)
   243 
   244 fun count_combterm (CombConst ((c, _), _, _)) =
   245     Symtab.map_entry c (Integer.add 1)
   246   | count_combterm (CombVar _) = I
   247   | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
   248 fun count_literal (Literal (_, t)) = count_combterm t
   249 fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
   250 
   251 fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
   252 fun cnf_helper_thms thy raw =
   253   map (`Thm.get_name_hint)
   254   #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
   255 
   256 val optional_helpers =
   257   [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
   258    (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
   259    (["c_COMBS"], (false, @{thms COMBS_def}))]
   260 val optional_typed_helpers =
   261   [(["c_True", "c_False"], (true, @{thms True_or_False})),
   262    (["c_If"], (true, @{thms if_True if_False True_or_False}))]
   263 val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   264 
   265 val init_counters =
   266   Symtab.make (maps (maps (map (rpair 0) o fst))
   267                     [optional_helpers, optional_typed_helpers])
   268 
   269 fun get_helper_clauses thy is_FO full_types conjectures axcls =
   270   let
   271     val axclauses = map snd (make_axiom_clauses thy axcls)
   272     val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
   273     fun is_needed c = the (Symtab.lookup ct c) > 0
   274     val cnfs =
   275       (optional_helpers
   276        |> full_types ? append optional_typed_helpers
   277        |> maps (fn (ss, (raw, ths)) =>
   278                    if exists is_needed ss then cnf_helper_thms thy raw ths
   279                    else []))
   280       @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   281   in map snd (make_axiom_clauses thy cnfs) end
   282 
   283 fun make_clause_table xs =
   284   fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
   285 
   286 
   287 (***************************************************************)
   288 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   289 (***************************************************************)
   290 
   291 fun set_insert (x, s) = Symtab.update (x, ()) s
   292 
   293 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
   294 
   295 (*Remove this trivial type class*)
   296 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
   297 
   298 fun tfree_classes_of_terms ts =
   299   let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   300   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   301 
   302 fun tvar_classes_of_terms ts =
   303   let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   304   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   305 
   306 (*fold type constructors*)
   307 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   308   | fold_type_consts _ _ x = x;
   309 
   310 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   311 fun add_type_consts_in_term thy =
   312   let
   313     val const_typargs = Sign.const_typargs thy
   314     fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
   315       | aux (Abs (_, _, u)) = aux u
   316       | aux (Const (@{const_name skolem_id}, _) $ _) = I
   317       | aux (t $ u) = aux t #> aux u
   318       | aux _ = I
   319   in aux end
   320 
   321 fun type_consts_of_terms thy ts =
   322   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   323 
   324 (* Remove existing axiom clauses from the conjecture clauses, as this can
   325    dramatically boost an ATP's performance (for some reason). *)
   326 fun subtract_cls ax_clauses =
   327   filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
   328 
   329 (* prepare for passing to writer,
   330    create additional clauses based on the information from extra_cls *)
   331 fun prepare_clauses full_types goal_cls axcls extra_cls thy =
   332   let
   333     val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
   334     val ccls = subtract_cls extra_cls goal_cls
   335     val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   336     val ccltms = map prop_of ccls
   337     and axtms = map (prop_of o #1) extra_cls
   338     val subs = tfree_classes_of_terms ccltms
   339     and supers = tvar_classes_of_terms axtms
   340     and tycons = type_consts_of_terms thy (ccltms @ axtms)
   341     (*TFrees in conjecture clauses; TVars in axiom clauses*)
   342     val conjectures = make_conjecture_clauses thy ccls
   343     val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
   344     val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
   345     val helper_clauses =
   346       get_helper_clauses thy is_FO full_types conjectures extra_cls
   347     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   348     val classrel_clauses = make_classrel_clauses thy subs supers'
   349   in
   350     (Vector.fromList clnames,
   351       (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   352   end
   353 
   354 end;