src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
author blanchet
Fri Apr 16 15:49:13 2010 +0200 (2010-04-16)
changeset 36170 0cdb76723c88
parent 36169 27b1cc58715e
child 36186 bd246b00ef5a
permissions -rw-r--r--
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet@35826
     1
(*  Title:      HOL/Sledgehammer/sledgehammer_hol_clause.ML
wenzelm@33311
     2
    Author:     Jia Meng, NICTA
mengj@17998
     3
wenzelm@24311
     4
FOL clauses translated from HOL formulae.
mengj@17998
     5
*)
mengj@17998
     6
blanchet@35826
     7
signature SLEDGEHAMMER_HOL_CLAUSE =
wenzelm@24311
     8
sig
blanchet@36170
     9
  type name = Sledgehammer_FOL_Clause.name
blanchet@35865
    10
  type kind = Sledgehammer_FOL_Clause.kind
blanchet@35865
    11
  type fol_type = Sledgehammer_FOL_Clause.fol_type
blanchet@35865
    12
  type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
blanchet@35865
    13
  type arity_clause = Sledgehammer_FOL_Clause.arity_clause
wenzelm@24311
    14
  type axiom_name = string
wenzelm@24311
    15
  type polarity = bool
blanchet@35865
    16
  type hol_clause_id = int
blanchet@35865
    17
wenzelm@24311
    18
  datatype combterm =
blanchet@36170
    19
    CombConst of name * fol_type * fol_type list (* Const and Free *) |
blanchet@36170
    20
    CombVar of name * fol_type |
blanchet@35865
    21
    CombApp of combterm * combterm
wenzelm@24311
    22
  datatype literal = Literal of polarity * combterm
blanchet@35865
    23
  datatype hol_clause =
blanchet@35865
    24
    HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
blanchet@35865
    25
                  kind: kind, literals: literal list, ctypes_sorts: typ list}
blanchet@35865
    26
blanchet@35865
    27
  val type_of_combterm : combterm -> fol_type
blanchet@35865
    28
  val strip_combterm_comb : combterm -> combterm * combterm list
blanchet@35865
    29
  val literals_of_term : theory -> term -> literal list * typ list
blanchet@35865
    30
  exception TRIVIAL
blanchet@35865
    31
  val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
blanchet@35865
    32
  val make_axiom_clauses : bool -> theory ->
blanchet@35865
    33
       (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
blanchet@35865
    34
  val get_helper_clauses : bool -> theory -> bool ->
blanchet@35865
    35
       hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
blanchet@35865
    36
       hol_clause list
blanchet@36169
    37
  val write_tptp_file : bool -> bool -> Path.T ->
blanchet@35865
    38
    hol_clause list * hol_clause list * hol_clause list * hol_clause list *
blanchet@35865
    39
    classrel_clause list * arity_clause list ->
immler@31839
    40
    int * int
blanchet@36169
    41
  val write_dfg_file : bool -> bool -> Path.T ->
blanchet@35865
    42
    hol_clause list * hol_clause list * hol_clause list * hol_clause list *
blanchet@35865
    43
    classrel_clause list * arity_clause list -> int * int
wenzelm@24311
    44
end
mengj@17998
    45
blanchet@35826
    46
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
mengj@17998
    47
struct
mengj@17998
    48
blanchet@36167
    49
open Sledgehammer_Util
blanchet@35865
    50
open Sledgehammer_FOL_Clause
blanchet@35865
    51
open Sledgehammer_Fact_Preprocessor
paulson@22825
    52
blanchet@35963
    53
(* Parameter "full_types" below indicates that full type information is to be
nipkow@31800
    54
exported *)
paulson@22825
    55
blanchet@35865
    56
(* If true, each function will be directly applied to as many arguments as
blanchet@35865
    57
   possible, avoiding use of the "apply" operator. Use of hBOOL is also
blanchet@35865
    58
   minimized. *)
wenzelm@30153
    59
val minimize_applies = true;
paulson@22064
    60
wenzelm@33035
    61
fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
paulson@22064
    62
paulson@22825
    63
(*True if the constant ever appears outside of the top-level position in literals.
paulson@22825
    64
  If false, the constant always receives all of its arguments and is used as a predicate.*)
wenzelm@33035
    65
fun needs_hBOOL const_needs_hBOOL c =
wenzelm@33035
    66
  not minimize_applies orelse
wenzelm@33035
    67
    the_default false (Symtab.lookup const_needs_hBOOL c);
paulson@22064
    68
mengj@19198
    69
mengj@17998
    70
(******************************************************)
mengj@17998
    71
(* data types for typed combinator expressions        *)
mengj@17998
    72
(******************************************************)
mengj@17998
    73
mengj@17998
    74
type axiom_name = string;
mengj@17998
    75
type polarity = bool;
blanchet@35865
    76
type hol_clause_id = int;
mengj@17998
    77
blanchet@35865
    78
datatype combterm =
blanchet@36170
    79
  CombConst of name * fol_type * fol_type list (* Const and Free *) |
blanchet@36170
    80
  CombVar of name * fol_type |
blanchet@35865
    81
  CombApp of combterm * combterm
wenzelm@24311
    82
mengj@17998
    83
datatype literal = Literal of polarity * combterm;
mengj@17998
    84
blanchet@35865
    85
datatype hol_clause =
blanchet@35865
    86
  HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
blanchet@35865
    87
                kind: kind, literals: literal list, ctypes_sorts: typ list};
mengj@17998
    88
mengj@17998
    89
mengj@17998
    90
(*********************************************************************)
mengj@17998
    91
(* convert a clause with type Term.term to a clause with type clause *)
mengj@17998
    92
(*********************************************************************)
mengj@17998
    93
blanchet@36170
    94
fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
blanchet@35865
    95
      (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
mengj@17998
    96
  | isFalse _ = false;
mengj@17998
    97
blanchet@36170
    98
fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
mengj@17998
    99
      (pol andalso c = "c_True") orelse
mengj@17998
   100
      (not pol andalso c = "c_False")
mengj@17998
   101
  | isTrue _ = false;
wenzelm@24311
   102
blanchet@35865
   103
fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
mengj@17998
   104
immler@30151
   105
fun type_of dfg (Type (a, Ts)) =
blanchet@36169
   106
    let val (folTypes,ts) = types_of dfg Ts in
blanchet@36169
   107
      (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts)
blanchet@36169
   108
    end
blanchet@36169
   109
  | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
blanchet@36169
   110
  | type_of _ (tp as TVar (x, _)) =
blanchet@36169
   111
    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
immler@30151
   112
and types_of dfg Ts =
immler@30151
   113
      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
blanchet@35865
   114
      in  (folTyps, union_all ts)  end;
mengj@17998
   115
mengj@17998
   116
(* same as above, but no gathering of sort information *)
immler@30151
   117
fun simp_type_of dfg (Type (a, Ts)) =
blanchet@36169
   118
      TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts)
blanchet@36169
   119
  | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a)
blanchet@36169
   120
  | simp_type_of _ (TVar (x, _)) =
blanchet@36169
   121
    TyVar (make_schematic_type_var x, string_of_indexname x);
mengj@18440
   122
mengj@18356
   123
immler@30151
   124
fun const_type_of dfg thy (c,t) =
immler@30151
   125
      let val (tp,ts) = type_of dfg t
immler@30151
   126
      in  (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
mengj@18356
   127
mengj@17998
   128
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
immler@30151
   129
fun combterm_of dfg thy (Const(c,t)) =
immler@30151
   130
      let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
blanchet@36170
   131
          val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
paulson@22078
   132
      in  (c',ts)  end
wenzelm@32994
   133
  | combterm_of dfg _ (Free(v,t)) =
immler@30151
   134
      let val (tp,ts) = type_of dfg t
blanchet@36170
   135
          val v' = CombConst (`make_fixed_var v, tp, [])
paulson@22078
   136
      in  (v',ts)  end
wenzelm@32994
   137
  | combterm_of dfg _ (Var(v,t)) =
immler@30151
   138
      let val (tp,ts) = type_of dfg t
blanchet@36170
   139
          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
paulson@22078
   140
      in  (v',ts)  end
immler@30151
   141
  | combterm_of dfg thy (P $ Q) =
immler@30151
   142
      let val (P',tsP) = combterm_of dfg thy P
immler@30151
   143
          val (Q',tsQ) = combterm_of dfg thy Q
haftmann@33042
   144
      in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
blanchet@35865
   145
  | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
mengj@17998
   146
blanchet@35865
   147
fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
immler@30151
   148
  | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
mengj@17998
   149
blanchet@35865
   150
fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
blanchet@35865
   151
  | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
immler@30151
   152
      literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
immler@30151
   153
  | literals_of_term1 dfg thy (lits,ts) P =
immler@30151
   154
      let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
paulson@21509
   155
      in
haftmann@33042
   156
          (Literal(pol,pred)::lits, union (op =) ts ts')
paulson@21509
   157
      end;
mengj@17998
   158
immler@30151
   159
fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
immler@30151
   160
val literals_of_term = literals_of_term_dfg false;
mengj@17998
   161
blanchet@35865
   162
(* Trivial problem, which resolution cannot handle (empty clause) *)
blanchet@35865
   163
exception TRIVIAL;
wenzelm@28835
   164
mengj@17998
   165
(* making axiom and conjecture clauses *)
blanchet@35865
   166
fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
immler@30151
   167
    let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
mengj@17998
   168
    in
blanchet@35865
   169
        if forall isFalse lits then
blanchet@35865
   170
            raise TRIVIAL
wenzelm@24311
   171
        else
blanchet@35865
   172
            HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
blanchet@35865
   173
                       kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
mengj@17998
   174
    end;
mengj@17998
   175
mengj@20016
   176
immler@30151
   177
fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
blanchet@35865
   178
  let val cls = make_clause dfg thy (id, name, Axiom, th)
paulson@21573
   179
  in
paulson@21573
   180
      if isTaut cls then pairs else (name,cls)::pairs
paulson@21573
   181
  end;
mengj@19354
   182
wenzelm@30190
   183
fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) [];
mengj@19354
   184
wenzelm@32994
   185
fun make_conjecture_clauses_aux _ _ _ [] = []
immler@30151
   186
  | make_conjecture_clauses_aux dfg thy n (th::ths) =
blanchet@35865
   187
      make_clause dfg thy (n,"conjecture", Conjecture, th) ::
immler@30151
   188
      make_conjecture_clauses_aux dfg thy (n+1) ths;
mengj@17998
   189
immler@30151
   190
fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
mengj@17998
   191
mengj@17998
   192
mengj@17998
   193
(**********************************************************************)
mengj@17998
   194
(* convert clause into ATP specific formats:                          *)
mengj@17998
   195
(* TPTP used by Vampire and E                                         *)
mengj@19720
   196
(* DFG used by SPASS                                                  *)
mengj@17998
   197
(**********************************************************************)
mengj@17998
   198
paulson@22078
   199
(*Result of a function type; no need to check that the argument type matches.*)
blanchet@36169
   200
fun result_type (TyConstr (("tc_fun", _), [_, tp2])) = tp2
blanchet@36168
   201
  | result_type _ = raise Fail "Non-function type"
paulson@22078
   202
wenzelm@32994
   203
fun type_of_combterm (CombConst (_, tp, _)) = tp
wenzelm@32994
   204
  | type_of_combterm (CombVar (_, tp)) = tp
wenzelm@32994
   205
  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
mengj@17998
   206
paulson@22064
   207
(*gets the head of a combinator application, along with the list of arguments*)
blanchet@35865
   208
fun strip_combterm_comb u =
paulson@22078
   209
    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
paulson@22064
   210
        |   stripc  x =  x
paulson@22064
   211
    in  stripc(u,[])  end;
paulson@22064
   212
paulson@22851
   213
val type_wrapper = "ti";
paulson@22851
   214
blanchet@36170
   215
fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) =
blanchet@36170
   216
    needs_hBOOL const_needs_hBOOL c
wenzelm@32994
   217
  | head_needs_hBOOL _ _ = true;
paulson@22851
   218
blanchet@36170
   219
fun wrap_type full_types (s, ty) pool =
blanchet@36170
   220
  if full_types then
blanchet@36170
   221
    let val (s', pool) = string_of_fol_type ty pool in
blanchet@36170
   222
      (type_wrapper ^ paren_pack [s, s'], pool)
blanchet@36170
   223
    end
blanchet@36170
   224
  else
blanchet@36170
   225
    (s, pool)
blanchet@36170
   226
blanchet@36170
   227
fun wrap_type_if full_types cnh (head, s, tp) =
blanchet@36170
   228
  if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s
wenzelm@24311
   229
blanchet@35865
   230
fun apply ss = "hAPP" ^ paren_pack ss;
paulson@22851
   231
paulson@22064
   232
fun rev_apply (v, []) = v
paulson@22851
   233
  | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
paulson@22064
   234
paulson@22064
   235
fun string_apply (v, args) = rev_apply (v, rev args);
paulson@22064
   236
blanchet@36170
   237
(* Apply an operator to the argument strings, using either the "apply" operator
blanchet@36170
   238
   or direct function application. *)
blanchet@36170
   239
fun string_of_application full_types cma (CombConst ((s, s'), _, tvars), args)
blanchet@36170
   240
                          pool =
blanchet@36170
   241
    let
blanchet@36170
   242
      val s = if s = "equal" then "c_fequal" else s
blanchet@36170
   243
      val nargs = min_arity_of cma s
blanchet@36170
   244
      val args1 = List.take (args, nargs)
blanchet@36170
   245
        handle Subscript =>
blanchet@36170
   246
               raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
blanchet@36170
   247
                           " but is applied to " ^ commas (map quote args))
blanchet@36170
   248
      val args2 = List.drop (args, nargs)
blanchet@36170
   249
      val (targs, pool) = if full_types then ([], pool)
blanchet@36170
   250
                          else pool_map string_of_fol_type tvars pool
blanchet@36170
   251
      val (s, pool) = nice_name (s, s') pool
blanchet@36170
   252
    in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
blanchet@36170
   253
  | string_of_application _ _ (CombVar (name, _), args) pool =
blanchet@36170
   254
    nice_name name pool |>> (fn s => string_apply (s, args))
wenzelm@24311
   255
blanchet@36170
   256
fun string_of_combterm (params as (full_types, cma, cnh)) t pool =
blanchet@36170
   257
  let
blanchet@36170
   258
    val (head, args) = strip_combterm_comb t
blanchet@36170
   259
    val (ss, pool) = pool_map (string_of_combterm params) args pool
blanchet@36170
   260
    val (s, pool) = string_of_application full_types cma (head, ss) pool
blanchet@36170
   261
  in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end
mengj@18356
   262
paulson@22064
   263
(*Boolean-valued terms are here converted to literals.*)
blanchet@36170
   264
fun boolify params c =
blanchet@36170
   265
  string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
paulson@22064
   266
blanchet@36170
   267
fun string_of_predicate (params as (_, _, cnh)) t =
paulson@22064
   268
  case t of
blanchet@36170
   269
    (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
blanchet@36170
   270
    (* DFG only: new TPTP prefers infix equality *)
blanchet@36170
   271
    pool_map (string_of_combterm params) [t1, t2]
blanchet@36170
   272
    #>> prefix "equal" o paren_pack
blanchet@36170
   273
  | _ =>
blanchet@36170
   274
    case #1 (strip_combterm_comb t) of
blanchet@36170
   275
      CombConst ((s, _), _, _) =>
blanchet@36170
   276
      (if needs_hBOOL cnh s then boolify else string_of_combterm) params t
blanchet@36170
   277
    | _ => boolify params t
mengj@18356
   278
mengj@17998
   279
blanchet@36170
   280
(*** TPTP format ***)
mengj@19720
   281
blanchet@36170
   282
fun tptp_of_equality params pos (t1, t2) =
blanchet@36170
   283
  pool_map (string_of_combterm params) [t1, t2]
blanchet@36170
   284
  #>> space_implode (if pos then " = " else " != ")
wenzelm@24311
   285
blanchet@36170
   286
fun tptp_literal params
blanchet@36170
   287
        (Literal (pos, CombApp (CombApp (CombConst (("equal", _), _, _), t1),
blanchet@36170
   288
                                         t2))) =
blanchet@36170
   289
    tptp_of_equality params pos (t1, t2)
blanchet@36170
   290
  | tptp_literal params (Literal (pos, pred)) =
blanchet@36170
   291
    string_of_predicate params pred #>> tptp_sign pos
blanchet@36170
   292
 
blanchet@36170
   293
(* Given a clause, returns its literals paired with a list of literals
blanchet@36170
   294
   concerning TFrees; the latter should only occur in conjecture clauses. *)
blanchet@36170
   295
fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
blanchet@36170
   296
  pool_map (tptp_literal params) literals
blanchet@36170
   297
  #>> rpair (map (tptp_of_typeLit pos) (add_typs ctypes_sorts))
wenzelm@24311
   298
blanchet@36170
   299
fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
blanchet@36170
   300
                pool =
blanchet@36170
   301
let
blanchet@36170
   302
    val ((lits, tylits), pool) =
blanchet@36170
   303
      tptp_type_literals params (kind = Conjecture) cls pool
paulson@24937
   304
  in
blanchet@36170
   305
    ((gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits), pool)
blanchet@36170
   306
  end
mengj@17998
   307
mengj@17998
   308
blanchet@36170
   309
(*** DFG format ***)
paulson@21561
   310
blanchet@36170
   311
fun dfg_literal params (Literal (pos, pred)) =
blanchet@36170
   312
  string_of_predicate params pred #>> dfg_sign pos
mengj@19720
   313
blanchet@36170
   314
fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
blanchet@36170
   315
  pool_map (dfg_literal params) literals
blanchet@36170
   316
  #>> rpair (map (dfg_of_typeLit pos) (add_typs ctypes_sorts))
mengj@19720
   317
blanchet@36170
   318
fun get_uvars (CombConst _) vars pool = (vars, pool)
blanchet@36170
   319
  | get_uvars (CombVar (name, _)) vars pool =
blanchet@36170
   320
    nice_name name pool |>> (fn var => var :: vars)
blanchet@36170
   321
  | get_uvars (CombApp (P, Q)) vars pool =
blanchet@36170
   322
    let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end
mengj@19720
   323
blanchet@36170
   324
fun get_uvars_l (Literal (_, c)) = get_uvars c [];
mengj@19720
   325
blanchet@36170
   326
fun dfg_vars (HOLClause {literals, ...}) =
blanchet@36170
   327
  pool_map get_uvars_l literals #>> union_all
wenzelm@24311
   328
blanchet@36170
   329
fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind,
blanchet@36170
   330
                                         ctypes_sorts, ...}) pool =
blanchet@36170
   331
  let
blanchet@36170
   332
    val ((lits, tylits), pool) =
blanchet@36170
   333
      dfg_type_literals params (kind = Conjecture) cls pool
blanchet@36170
   334
    val (vars, pool) = dfg_vars cls pool
blanchet@36170
   335
    val tvars = get_tvar_strs ctypes_sorts
paulson@24937
   336
  in
blanchet@36170
   337
    ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars),
blanchet@36170
   338
      tylits), pool)
blanchet@36170
   339
  end
paulson@24937
   340
mengj@19720
   341
paulson@22064
   342
(** For DFG format: accumulate function and predicate declarations **)
mengj@19720
   343
blanchet@35865
   344
fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
mengj@19720
   345
blanchet@36170
   346
fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars), (funcs, preds)) =
blanchet@36170
   347
      if c = "equal" then
blanchet@36170
   348
        (addtypes tvars funcs, preds)
paulson@21561
   349
      else
wenzelm@32960
   350
        let val arity = min_arity_of cma c
blanchet@35963
   351
            val ntys = if not full_types then length tvars else 0
wenzelm@32960
   352
            val addit = Symtab.update(c, arity+ntys)
wenzelm@32960
   353
        in
wenzelm@32960
   354
            if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
wenzelm@32960
   355
            else (addtypes tvars funcs, addit preds)
wenzelm@32960
   356
        end
blanchet@36170
   357
  | add_decls _ (CombVar (_,ctp), (funcs, preds)) =
blanchet@35865
   358
      (add_foltype_funcs (ctp,funcs), preds)
nipkow@31800
   359
  | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
mengj@19720
   360
blanchet@35865
   361
fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls);
mengj@19720
   362
blanchet@35865
   363
fun add_clause_decls params (HOLClause {literals, ...}, decls) =
nipkow@31800
   364
    List.foldl (add_literal_decls params) decls literals
wenzelm@27187
   365
    handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
mengj@19720
   366
nipkow@31800
   367
fun decls_of_clauses params clauses arity_clauses =
blanchet@35865
   368
  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab)
paulson@22064
   369
      val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
nipkow@31800
   370
      val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
paulson@22064
   371
  in
blanchet@35865
   372
      (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses),
paulson@22064
   373
       Symtab.dest predtab)
paulson@22064
   374
  end;
mengj@19720
   375
blanchet@35865
   376
fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) =
blanchet@35865
   377
  List.foldl add_type_sort_preds preds ctypes_sorts
wenzelm@27187
   378
  handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
paulson@21398
   379
paulson@21398
   380
(*Higher-order clauses have only the predicates hBOOL and type classes.*)
wenzelm@24311
   381
fun preds_of_clauses clauses clsrel_clauses arity_clauses =
mengj@19720
   382
    Symtab.dest
blanchet@35865
   383
        (List.foldl add_classrel_clause_preds
blanchet@35865
   384
               (List.foldl add_arity_clause_preds
wenzelm@30190
   385
                      (List.foldl add_clause_preds Symtab.empty clauses)
wenzelm@24311
   386
                      arity_clauses)
wenzelm@24311
   387
               clsrel_clauses)
mengj@19720
   388
mengj@18440
   389
mengj@18440
   390
(**********************************************************************)
mengj@19198
   391
(* write clauses to files                                             *)
mengj@19198
   392
(**********************************************************************)
mengj@19198
   393
paulson@21573
   394
val init_counters =
blanchet@35865
   395
  Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
blanchet@35865
   396
               ("c_COMBS", 0)];
wenzelm@24311
   397
blanchet@36170
   398
fun count_combterm (CombConst ((c, _), _, _), ct) =
paulson@21573
   399
     (case Symtab.lookup ct c of NONE => ct  (*no counter*)
paulson@21573
   400
                               | SOME n => Symtab.update (c,n+1) ct)
wenzelm@32994
   401
  | count_combterm (CombVar _, ct) = ct
paulson@22078
   402
  | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
paulson@21573
   403
paulson@21573
   404
fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
paulson@21573
   405
blanchet@35865
   406
fun count_clause (HOLClause {literals, ...}, ct) =
blanchet@35865
   407
  List.foldl count_literal ct literals;
paulson@21573
   408
blanchet@35865
   409
fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) =
wenzelm@30190
   410
  if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
paulson@21573
   411
  else ct;
paulson@21573
   412
blanchet@35865
   413
fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname
mengj@20644
   414
immler@31752
   415
fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
blanchet@35865
   416
  if isFO then
blanchet@35865
   417
    []
paulson@23386
   418
  else
immler@31752
   419
    let
immler@31752
   420
        val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
immler@31752
   421
        val ct0 = List.foldl count_clause init_counters conjectures
wenzelm@30190
   422
        val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
wenzelm@33035
   423
        fun needed c = the (Symtab.lookup ct c) > 0
wenzelm@24311
   424
        val IK = if needed "c_COMBI" orelse needed "c_COMBK"
blanchet@35865
   425
                 then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
wenzelm@24311
   426
                 else []
wenzelm@24311
   427
        val BC = if needed "c_COMBB" orelse needed "c_COMBC"
blanchet@35865
   428
                 then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}]
paulson@21135
   429
                 else []
blanchet@35865
   430
        val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}]
wenzelm@24311
   431
                else []
blanchet@35865
   432
        val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
blanchet@35865
   433
                                         @{thm equal_imp_fequal}]
mengj@20791
   434
    in
immler@30151
   435
        map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
paulson@23386
   436
    end;
mengj@20791
   437
paulson@22064
   438
(*Find the minimal arity of each function mentioned in the term. Also, note which uses
paulson@22064
   439
  are not at top level, to see if hBOOL is needed.*)
immler@30150
   440
fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
blanchet@35865
   441
  let val (head, args) = strip_combterm_comb t
paulson@22064
   442
      val n = length args
immler@30150
   443
      val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
paulson@22064
   444
  in
paulson@22064
   445
      case head of
blanchet@36170
   446
          CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
wenzelm@24311
   447
            let val a = if a="equal" andalso not toplev then "c_fequal" else a
wenzelm@33029
   448
            val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
wenzelm@24311
   449
            in
immler@30150
   450
              if toplev then (const_min_arity, const_needs_hBOOL)
immler@30150
   451
              else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
wenzelm@24311
   452
            end
wenzelm@32994
   453
        | _ => (const_min_arity, const_needs_hBOOL)
paulson@22064
   454
  end;
paulson@22064
   455
paulson@22064
   456
(*A literal is a top-level term*)
immler@30150
   457
fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
immler@30150
   458
  count_constants_term true t (const_min_arity, const_needs_hBOOL);
paulson@22064
   459
blanchet@35865
   460
fun count_constants_clause (HOLClause {literals, ...})
blanchet@35865
   461
                           (const_min_arity, const_needs_hBOOL) =
immler@30150
   462
  fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
paulson@22064
   463
immler@30150
   464
fun display_arity const_needs_hBOOL (c,n) =
blanchet@35865
   465
  trace_msg (fn () => "Constant: " ^ c ^
blanchet@35826
   466
                " arity:\t" ^ Int.toString n ^
immler@30150
   467
                (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
paulson@22064
   468
immler@31865
   469
fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
wenzelm@30153
   470
  if minimize_applies then
immler@30150
   471
     let val (const_min_arity, const_needs_hBOOL) =
immler@30150
   472
          fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
immler@31865
   473
       |> fold count_constants_clause extra_clauses
immler@30149
   474
       |> fold count_constants_clause helper_clauses
immler@30150
   475
     val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
immler@30150
   476
     in (const_min_arity, const_needs_hBOOL) end
immler@30150
   477
  else (Symtab.empty, Symtab.empty);
paulson@22064
   478
blanchet@35865
   479
(* TPTP format *)
immler@31749
   480
blanchet@36169
   481
fun write_tptp_file debug full_types file clauses =
immler@31409
   482
  let
blanchet@36167
   483
    fun section _ [] = []
blanchet@36167
   484
      | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
blanchet@36170
   485
    val pool = empty_name_pool debug
immler@31865
   486
    val (conjectures, axclauses, _, helper_clauses,
immler@31865
   487
      classrel_clauses, arity_clauses) = clauses
nipkow@31791
   488
    val (cma, cnh) = count_constants clauses
blanchet@35963
   489
    val params = (full_types, cma, cnh)
blanchet@36170
   490
    val ((conjecture_clss, tfree_litss), pool) =
blanchet@36170
   491
      pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
blanchet@35865
   492
    val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
blanchet@36170
   493
    val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses
blanchet@36170
   494
                                   pool
blanchet@36170
   495
    val classrel_clss = map tptp_classrel_clause classrel_clauses
blanchet@36170
   496
    val arity_clss = map tptp_arity_clause arity_clauses
blanchet@36170
   497
    val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params)
blanchet@36170
   498
                                       helper_clauses pool
immler@31839
   499
    val _ =
immler@31839
   500
      File.write_list file (
blanchet@36167
   501
        "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
blanchet@36170
   502
        "% " ^ timestamp () ^ "\n" ::
blanchet@36170
   503
        section "Relevant fact" ax_clss @
blanchet@36167
   504
        section "Type variable" tfree_clss @
blanchet@36170
   505
        section "Class relationship" classrel_clss @
blanchet@36170
   506
        section "Arity declaration" arity_clss @
blanchet@36170
   507
        section "Helper fact" helper_clss @
blanchet@36170
   508
        section "Conjecture" conjecture_clss)
blanchet@36170
   509
    in (length axclauses + 1, length tfree_clss + length conjecture_clss)
immler@31409
   510
  end;
mengj@19198
   511
mengj@19720
   512
blanchet@35865
   513
(* DFG format *)
mengj@19720
   514
blanchet@36169
   515
fun write_dfg_file debug full_types file clauses =
immler@31409
   516
  let
blanchet@36170
   517
    val pool = empty_name_pool debug
immler@31865
   518
    val (conjectures, axclauses, _, helper_clauses,
immler@31865
   519
      classrel_clauses, arity_clauses) = clauses
nipkow@31791
   520
    val (cma, cnh) = count_constants clauses
blanchet@35963
   521
    val params = (full_types, cma, cnh)
blanchet@36170
   522
    val ((conjecture_clss, tfree_litss), pool) =
blanchet@36170
   523
      pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
immler@31838
   524
    and probname = Path.implode (Path.base file)
blanchet@36170
   525
    val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
blanchet@35865
   526
    val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
blanchet@36170
   527
    val (helper_clauses_strs, pool) =
blanchet@36170
   528
      pool_map (apfst fst oo dfg_clause params) helper_clauses pool
nipkow@31791
   529
    val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
immler@31409
   530
    and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
immler@31839
   531
    val _ =
immler@31839
   532
      File.write_list file (
blanchet@35865
   533
        string_of_start probname ::
blanchet@35865
   534
        string_of_descrip probname ::
blanchet@35865
   535
        string_of_symbols (string_of_funcs funcs)
blanchet@35865
   536
          (string_of_preds (cl_preds @ ty_preds)) ::
blanchet@36167
   537
        "list_of_clauses(axioms, cnf).\n" ::
immler@31839
   538
        axstrs @
blanchet@35865
   539
        map dfg_classrel_clause classrel_clauses @
blanchet@35865
   540
        map dfg_arity_clause arity_clauses @
immler@31839
   541
        helper_clauses_strs @
blanchet@36167
   542
        ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
immler@31839
   543
        tfree_clss @
blanchet@36170
   544
        conjecture_clss @
immler@31839
   545
        ["end_of_list.\n\n",
immler@31839
   546
        (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
blanchet@36167
   547
         "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n",
immler@31839
   548
         "end_problem.\n"])
immler@31839
   549
blanchet@36170
   550
  in
blanchet@36170
   551
    (length axclauses + length classrel_clauses + length arity_clauses +
blanchet@36170
   552
     length helper_clauses + 1, length tfree_clss + length conjecture_clss)
blanchet@36170
   553
  end
mengj@19720
   554
wenzelm@33311
   555
end;