src/HOL/Tools/ATP/atp_translate.ML
author blanchet
Wed Jun 08 16:20:18 2011 +0200 (2011-06-08)
changeset 43293 a80cdc4b27a3
parent 43289 0f2bbcfaf208
child 43295 30aaab778416
permissions -rw-r--r--
made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
blanchet@40114
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
blanchet@38282
     2
    Author:     Fabian Immler, TU Muenchen
blanchet@38282
     3
    Author:     Makarius
blanchet@38282
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@38282
     5
blanchet@39494
     6
Translation of HOL to FOL for Sledgehammer.
blanchet@38282
     7
*)
blanchet@38282
     8
blanchet@43085
     9
signature ATP_TRANSLATE =
blanchet@38282
    10
sig
blanchet@42227
    11
  type 'a fo_term = 'a ATP_Problem.fo_term
blanchet@43136
    12
  type connective = ATP_Problem.connective
blanchet@43136
    13
  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
blanchet@42939
    14
  type format = ATP_Problem.format
blanchet@42709
    15
  type formula_kind = ATP_Problem.formula_kind
blanchet@38282
    16
  type 'a problem = 'a ATP_Problem.problem
blanchet@43085
    17
blanchet@43085
    18
  type name = string * string
blanchet@43085
    19
blanchet@43085
    20
  datatype type_literal =
blanchet@43085
    21
    TyLitVar of name * name |
blanchet@43085
    22
    TyLitFree of name * name
blanchet@43085
    23
blanchet@43085
    24
  datatype arity_literal =
blanchet@43085
    25
    TConsLit of name * name * name list |
blanchet@43085
    26
    TVarLit of name * name
blanchet@43085
    27
blanchet@43086
    28
  type arity_clause =
blanchet@43086
    29
    {name: string,
blanchet@43086
    30
     prem_lits: arity_literal list,
blanchet@43086
    31
     concl_lits: arity_literal}
blanchet@43085
    32
blanchet@43086
    33
  type class_rel_clause =
blanchet@43086
    34
    {name: string,
blanchet@43086
    35
     subclass: name,
blanchet@43086
    36
     superclass: name}
blanchet@43085
    37
blanchet@43085
    38
  datatype combterm =
blanchet@43085
    39
    CombConst of name * typ * typ list |
blanchet@43085
    40
    CombVar of name * typ |
blanchet@43085
    41
    CombApp of combterm * combterm
blanchet@43085
    42
blanchet@43085
    43
  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
blanchet@42613
    44
blanchet@42613
    45
  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
blanchet@42613
    46
  datatype type_level =
blanchet@42613
    47
    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
blanchet@43128
    48
  datatype type_heaviness = Heavyweight | Lightweight
blanchet@42613
    49
blanchet@43102
    50
  datatype type_sys =
blanchet@42722
    51
    Simple_Types of type_level |
blanchet@42837
    52
    Preds of polymorphism * type_level * type_heaviness |
blanchet@42837
    53
    Tags of polymorphism * type_level * type_heaviness
blanchet@42613
    54
blanchet@43085
    55
  val bound_var_prefix : string
blanchet@43085
    56
  val schematic_var_prefix: string
blanchet@43085
    57
  val fixed_var_prefix: string
blanchet@43085
    58
  val tvar_prefix: string
blanchet@43085
    59
  val tfree_prefix: string
blanchet@43085
    60
  val const_prefix: string
blanchet@43085
    61
  val type_const_prefix: string
blanchet@43085
    62
  val class_prefix: string
blanchet@43085
    63
  val skolem_const_prefix : string
blanchet@43085
    64
  val old_skolem_const_prefix : string
blanchet@43085
    65
  val new_skolem_const_prefix : string
blanchet@43125
    66
  val type_decl_prefix : string
blanchet@43125
    67
  val sym_decl_prefix : string
blanchet@43125
    68
  val preds_sym_formula_prefix : string
blanchet@43129
    69
  val lightweight_tags_sym_formula_prefix : string
blanchet@40204
    70
  val fact_prefix : string
blanchet@38282
    71
  val conjecture_prefix : string
blanchet@42881
    72
  val helper_prefix : string
blanchet@43125
    73
  val class_rel_clause_prefix : string
blanchet@43125
    74
  val arity_clause_prefix : string
blanchet@43125
    75
  val tfree_clause_prefix : string
blanchet@42881
    76
  val typed_helper_suffix : string
blanchet@43125
    77
  val untyped_helper_suffix : string
blanchet@43159
    78
  val type_tag_idempotence_helper_name : string
blanchet@42966
    79
  val predicator_name : string
blanchet@42966
    80
  val app_op_name : string
blanchet@43104
    81
  val type_tag_name : string
blanchet@42966
    82
  val type_pred_name : string
blanchet@42962
    83
  val simple_type_prefix : string
blanchet@43174
    84
  val prefixed_predicator_name : string
blanchet@43130
    85
  val prefixed_app_op_name : string
blanchet@43130
    86
  val prefixed_type_tag_name : string
blanchet@43085
    87
  val ascii_of: string -> string
blanchet@43085
    88
  val unascii_of: string -> string
blanchet@43085
    89
  val strip_prefix_and_unascii : string -> string -> string option
blanchet@43159
    90
  val proxy_table : (string * (string * (thm * (string * string)))) list
blanchet@43159
    91
  val proxify_const : string -> (string * string) option
blanchet@43085
    92
  val invert_const: string -> string
blanchet@43085
    93
  val unproxify_const: string -> string
blanchet@43085
    94
  val make_bound_var : string -> string
blanchet@43085
    95
  val make_schematic_var : string * int -> string
blanchet@43085
    96
  val make_fixed_var : string -> string
blanchet@43085
    97
  val make_schematic_type_var : string * int -> string
blanchet@43085
    98
  val make_fixed_type_var : string -> string
blanchet@43085
    99
  val make_fixed_const : string -> string
blanchet@43085
   100
  val make_fixed_type_const : string -> string
blanchet@43085
   101
  val make_type_class : string -> string
blanchet@43093
   102
  val new_skolem_var_name_from_const : string -> string
blanchet@43093
   103
  val num_type_args : theory -> string -> int
blanchet@43248
   104
  val atp_irrelevant_consts : string list
blanchet@43248
   105
  val atp_schematic_consts_of : term -> typ list Symtab.table
blanchet@43085
   106
  val make_arity_clauses :
blanchet@43085
   107
    theory -> string list -> class list -> class list * arity_clause list
blanchet@43085
   108
  val make_class_rel_clauses :
blanchet@43085
   109
    theory -> class list -> class list -> class_rel_clause list
blanchet@43085
   110
  val combtyp_of : combterm -> typ
blanchet@43085
   111
  val strip_combterm_comb : combterm -> combterm * combterm list
blanchet@43085
   112
  val atyps_of : typ -> typ list
blanchet@43085
   113
  val combterm_from_term :
blanchet@43085
   114
    theory -> (string * typ) list -> term -> combterm * typ list
blanchet@43085
   115
  val is_locality_global : locality -> bool
blanchet@43102
   116
  val type_sys_from_string : string -> type_sys
blanchet@43102
   117
  val polymorphism_of_type_sys : type_sys -> polymorphism
blanchet@43102
   118
  val level_of_type_sys : type_sys -> type_level
blanchet@43102
   119
  val is_type_sys_virtually_sound : type_sys -> bool
blanchet@43102
   120
  val is_type_sys_fairly_sound : type_sys -> bool
blanchet@43102
   121
  val choose_format : format list -> type_sys -> format * type_sys
blanchet@43136
   122
  val mk_aconns :
blanchet@43136
   123
    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
blanchet@43130
   124
  val unmangled_const_name : string -> string
blanchet@42542
   125
  val unmangled_const : string -> string * string fo_term list
blanchet@43194
   126
  val helper_table : ((string * bool) * thm list) list
blanchet@43159
   127
  val should_specialize_helper : type_sys -> term -> bool
blanchet@43085
   128
  val tfree_classes_of_terms : term list -> string list
blanchet@43085
   129
  val tvar_classes_of_terms : term list -> string list
blanchet@43189
   130
  val type_constrs_of_terms : theory -> term list -> string list
blanchet@40059
   131
  val prepare_atp_problem :
blanchet@43102
   132
    Proof.context -> format -> formula_kind -> formula_kind -> type_sys
blanchet@43259
   133
    -> bool -> bool -> term list -> term -> ((string * locality) * term) list
blanchet@42541
   134
    -> string problem * string Symtab.table * int * int
blanchet@43214
   135
       * (string * locality) list vector * int list * int Symtab.table
blanchet@41313
   136
  val atp_problem_weights : string problem -> (string * real) list
blanchet@38282
   137
end;
blanchet@38282
   138
blanchet@43085
   139
structure ATP_Translate : ATP_TRANSLATE =
blanchet@38282
   140
struct
blanchet@38282
   141
blanchet@43085
   142
open ATP_Util
blanchet@38282
   143
open ATP_Problem
blanchet@43085
   144
blanchet@43085
   145
type name = string * string
blanchet@43085
   146
blanchet@42640
   147
(* experimental *)
blanchet@42640
   148
val generate_useful_info = false
blanchet@38282
   149
blanchet@42879
   150
fun useful_isabelle_info s =
blanchet@42879
   151
  if generate_useful_info then
blanchet@42879
   152
    SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
blanchet@42879
   153
  else
blanchet@42879
   154
    NONE
blanchet@42879
   155
blanchet@42879
   156
val intro_info = useful_isabelle_info "intro"
blanchet@42879
   157
val elim_info = useful_isabelle_info "elim"
blanchet@42879
   158
val simp_info = useful_isabelle_info "simp"
blanchet@42879
   159
blanchet@43085
   160
val bound_var_prefix = "B_"
blanchet@43085
   161
val schematic_var_prefix = "V_"
blanchet@43085
   162
val fixed_var_prefix = "v_"
blanchet@43085
   163
blanchet@43085
   164
val tvar_prefix = "T_"
blanchet@43085
   165
val tfree_prefix = "t_"
blanchet@43085
   166
blanchet@43085
   167
val const_prefix = "c_"
blanchet@43085
   168
val type_const_prefix = "tc_"
blanchet@43085
   169
val class_prefix = "cl_"
blanchet@43085
   170
blanchet@43085
   171
val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
blanchet@43085
   172
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
blanchet@43085
   173
val new_skolem_const_prefix = skolem_const_prefix ^ "n"
blanchet@43085
   174
blanchet@42998
   175
val type_decl_prefix = "ty_"
blanchet@42998
   176
val sym_decl_prefix = "sy_"
blanchet@43125
   177
val preds_sym_formula_prefix = "psy_"
blanchet@43129
   178
val lightweight_tags_sym_formula_prefix = "tsy_"
blanchet@40204
   179
val fact_prefix = "fact_"
blanchet@38282
   180
val conjecture_prefix = "conj_"
blanchet@38282
   181
val helper_prefix = "help_"
blanchet@43159
   182
val class_rel_clause_prefix = "clar_"
blanchet@38282
   183
val arity_clause_prefix = "arity_"
blanchet@43085
   184
val tfree_clause_prefix = "tfree_"
blanchet@38282
   185
blanchet@42881
   186
val typed_helper_suffix = "_T"
blanchet@42881
   187
val untyped_helper_suffix = "_U"
blanchet@43159
   188
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
blanchet@42881
   189
blanchet@42966
   190
val predicator_name = "hBOOL"
blanchet@42966
   191
val app_op_name = "hAPP"
blanchet@43104
   192
val type_tag_name = "ti"
blanchet@42966
   193
val type_pred_name = "is"
blanchet@42962
   194
val simple_type_prefix = "ty_"
blanchet@42531
   195
blanchet@43174
   196
val prefixed_predicator_name = const_prefix ^ predicator_name
blanchet@43130
   197
val prefixed_app_op_name = const_prefix ^ app_op_name
blanchet@43130
   198
val prefixed_type_tag_name = const_prefix ^ type_tag_name
blanchet@43130
   199
blanchet@38282
   200
(* Freshness almost guaranteed! *)
blanchet@38282
   201
val sledgehammer_weak_prefix = "Sledgehammer:"
blanchet@38282
   202
blanchet@43085
   203
(*Escaping of special characters.
blanchet@43085
   204
  Alphanumeric characters are left unchanged.
blanchet@43085
   205
  The character _ goes to __
blanchet@43085
   206
  Characters in the range ASCII space to / go to _A to _P, respectively.
blanchet@43085
   207
  Other characters go to _nnn where nnn is the decimal ASCII code.*)
blanchet@43093
   208
val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
blanchet@43085
   209
blanchet@43085
   210
fun stringN_of_int 0 _ = ""
blanchet@43085
   211
  | stringN_of_int k n =
blanchet@43085
   212
    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
blanchet@43085
   213
blanchet@43085
   214
fun ascii_of_char c =
blanchet@43085
   215
  if Char.isAlphaNum c then
blanchet@43085
   216
    String.str c
blanchet@43085
   217
  else if c = #"_" then
blanchet@43085
   218
    "__"
blanchet@43085
   219
  else if #" " <= c andalso c <= #"/" then
blanchet@43085
   220
    "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
blanchet@43085
   221
  else
blanchet@43085
   222
    (* fixed width, in case more digits follow *)
blanchet@43085
   223
    "_" ^ stringN_of_int 3 (Char.ord c)
blanchet@43085
   224
blanchet@43085
   225
val ascii_of = String.translate ascii_of_char
blanchet@43085
   226
blanchet@43085
   227
(** Remove ASCII armoring from names in proof files **)
blanchet@43085
   228
blanchet@43085
   229
(* We don't raise error exceptions because this code can run inside a worker
blanchet@43085
   230
   thread. Also, the errors are impossible. *)
blanchet@43085
   231
val unascii_of =
blanchet@43085
   232
  let
blanchet@43085
   233
    fun un rcs [] = String.implode(rev rcs)
blanchet@43085
   234
      | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
blanchet@43085
   235
        (* Three types of _ escapes: __, _A to _P, _nnn *)
blanchet@43085
   236
      | un rcs (#"_" :: #"_" :: cs) = un (#"_"::rcs) cs
blanchet@43085
   237
      | un rcs (#"_" :: c :: cs) =
blanchet@43085
   238
        if #"A" <= c andalso c<= #"P" then
blanchet@43085
   239
          (* translation of #" " to #"/" *)
blanchet@43085
   240
          un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
blanchet@43085
   241
        else
blanchet@43085
   242
          let val digits = List.take (c::cs, 3) handle Subscript => [] in
blanchet@43085
   243
            case Int.fromString (String.implode digits) of
blanchet@43085
   244
              SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
blanchet@43085
   245
            | NONE => un (c:: #"_"::rcs) cs (* ERROR *)
blanchet@43085
   246
          end
blanchet@43085
   247
      | un rcs (c :: cs) = un (c :: rcs) cs
blanchet@43085
   248
  in un [] o String.explode end
blanchet@43085
   249
blanchet@43085
   250
(* If string s has the prefix s1, return the result of deleting it,
blanchet@43085
   251
   un-ASCII'd. *)
blanchet@43085
   252
fun strip_prefix_and_unascii s1 s =
blanchet@43085
   253
  if String.isPrefix s1 s then
blanchet@43085
   254
    SOME (unascii_of (String.extract (s, size s1, NONE)))
blanchet@43085
   255
  else
blanchet@43085
   256
    NONE
blanchet@43085
   257
blanchet@43159
   258
val proxy_table =
blanchet@43159
   259
  [("c_False", (@{const_name False}, (@{thm fFalse_def},
blanchet@43159
   260
       ("fFalse", @{const_name ATP.fFalse})))),
blanchet@43159
   261
   ("c_True", (@{const_name True}, (@{thm fTrue_def},
blanchet@43159
   262
       ("fTrue", @{const_name ATP.fTrue})))),
blanchet@43159
   263
   ("c_Not", (@{const_name Not}, (@{thm fNot_def},
blanchet@43159
   264
       ("fNot", @{const_name ATP.fNot})))),
blanchet@43159
   265
   ("c_conj", (@{const_name conj}, (@{thm fconj_def},
blanchet@43159
   266
       ("fconj", @{const_name ATP.fconj})))),
blanchet@43159
   267
   ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
blanchet@43159
   268
       ("fdisj", @{const_name ATP.fdisj})))),
blanchet@43159
   269
   ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
blanchet@43159
   270
       ("fimplies", @{const_name ATP.fimplies})))),
blanchet@43159
   271
   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
blanchet@43159
   272
       ("fequal", @{const_name ATP.fequal}))))]
blanchet@43085
   273
blanchet@43159
   274
val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
blanchet@43085
   275
blanchet@43085
   276
(* Readable names for the more common symbolic functions. Do not mess with the
blanchet@43085
   277
   table unless you know what you are doing. *)
blanchet@43085
   278
val const_trans_table =
blanchet@43085
   279
  [(@{type_name Product_Type.prod}, "prod"),
blanchet@43085
   280
   (@{type_name Sum_Type.sum}, "sum"),
blanchet@43085
   281
   (@{const_name False}, "False"),
blanchet@43085
   282
   (@{const_name True}, "True"),
blanchet@43085
   283
   (@{const_name Not}, "Not"),
blanchet@43085
   284
   (@{const_name conj}, "conj"),
blanchet@43085
   285
   (@{const_name disj}, "disj"),
blanchet@43085
   286
   (@{const_name implies}, "implies"),
blanchet@43085
   287
   (@{const_name HOL.eq}, "equal"),
blanchet@43085
   288
   (@{const_name If}, "If"),
blanchet@43085
   289
   (@{const_name Set.member}, "member"),
blanchet@43085
   290
   (@{const_name Meson.COMBI}, "COMBI"),
blanchet@43085
   291
   (@{const_name Meson.COMBK}, "COMBK"),
blanchet@43085
   292
   (@{const_name Meson.COMBB}, "COMBB"),
blanchet@43085
   293
   (@{const_name Meson.COMBC}, "COMBC"),
blanchet@43085
   294
   (@{const_name Meson.COMBS}, "COMBS")]
blanchet@43085
   295
  |> Symtab.make
blanchet@43159
   296
  |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
blanchet@43085
   297
blanchet@43085
   298
(* Invert the table of translations between Isabelle and ATPs. *)
blanchet@43085
   299
val const_trans_table_inv =
blanchet@43085
   300
  const_trans_table |> Symtab.dest |> map swap |> Symtab.make
blanchet@43085
   301
val const_trans_table_unprox =
blanchet@43085
   302
  Symtab.empty
blanchet@43159
   303
  |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
blanchet@43085
   304
blanchet@43085
   305
val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
blanchet@43085
   306
val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
blanchet@43085
   307
blanchet@43085
   308
fun lookup_const c =
blanchet@43085
   309
  case Symtab.lookup const_trans_table c of
blanchet@43085
   310
    SOME c' => c'
blanchet@43085
   311
  | NONE => ascii_of c
blanchet@43085
   312
blanchet@43085
   313
(*Remove the initial ' character from a type variable, if it is present*)
blanchet@43085
   314
fun trim_type_var s =
blanchet@43085
   315
  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
blanchet@43085
   316
  else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
blanchet@43085
   317
blanchet@43085
   318
fun ascii_of_indexname (v,0) = ascii_of v
blanchet@43085
   319
  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i
blanchet@43085
   320
blanchet@43085
   321
fun make_bound_var x = bound_var_prefix ^ ascii_of x
blanchet@43085
   322
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
blanchet@43085
   323
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
blanchet@43085
   324
blanchet@43085
   325
fun make_schematic_type_var (x,i) =
blanchet@43085
   326
      tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i))
blanchet@43085
   327
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))
blanchet@43085
   328
blanchet@43085
   329
(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
blanchet@43085
   330
fun make_fixed_const @{const_name HOL.eq} = "equal"
blanchet@43085
   331
  | make_fixed_const c = const_prefix ^ lookup_const c
blanchet@43085
   332
blanchet@43085
   333
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
blanchet@43085
   334
blanchet@43085
   335
fun make_type_class clas = class_prefix ^ ascii_of clas
blanchet@43085
   336
blanchet@43093
   337
fun new_skolem_var_name_from_const s =
blanchet@43093
   338
  let val ss = s |> space_explode Long_Name.separator in
blanchet@43093
   339
    nth ss (length ss - 2)
blanchet@43093
   340
  end
blanchet@43093
   341
blanchet@43093
   342
(* The number of type arguments of a constant, zero if it's monomorphic. For
blanchet@43093
   343
   (instances of) Skolem pseudoconstants, this information is encoded in the
blanchet@43093
   344
   constant name. *)
blanchet@43093
   345
fun num_type_args thy s =
blanchet@43093
   346
  if String.isPrefix skolem_const_prefix s then
blanchet@43093
   347
    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
blanchet@43093
   348
  else
blanchet@43093
   349
    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
blanchet@43093
   350
blanchet@43248
   351
(* These are either simplified away by "Meson.presimplify" (most of the time) or
blanchet@43248
   352
   handled specially via "fFalse", "fTrue", ..., "fequal". *)
blanchet@43248
   353
val atp_irrelevant_consts =
blanchet@43248
   354
  [@{const_name False}, @{const_name True}, @{const_name Not},
blanchet@43248
   355
   @{const_name conj}, @{const_name disj}, @{const_name implies},
blanchet@43248
   356
   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
blanchet@43248
   357
blanchet@43248
   358
val atp_monomorph_bad_consts =
blanchet@43248
   359
  atp_irrelevant_consts @
blanchet@43248
   360
  (* These are ignored anyway by the relevance filter (unless they appear in
blanchet@43248
   361
     higher-order places) but not by the monomorphizer. *)
blanchet@43248
   362
  [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
blanchet@43248
   363
   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
blanchet@43248
   364
   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
blanchet@43248
   365
blanchet@43258
   366
fun add_schematic_const (x as (_, T)) =
blanchet@43258
   367
  Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
blanchet@43258
   368
val add_schematic_consts_of =
blanchet@43258
   369
  Term.fold_aterms (fn Const (x as (s, _)) =>
blanchet@43258
   370
                       not (member (op =) atp_monomorph_bad_consts s)
blanchet@43258
   371
                       ? add_schematic_const x
blanchet@43258
   372
                      | _ => I)
blanchet@43258
   373
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
blanchet@43248
   374
blanchet@43085
   375
(** Definitions and functions for FOL clauses and formulas for TPTP **)
blanchet@43085
   376
blanchet@43085
   377
(* The first component is the type class; the second is a "TVar" or "TFree". *)
blanchet@43085
   378
datatype type_literal =
blanchet@43085
   379
  TyLitVar of name * name |
blanchet@43085
   380
  TyLitFree of name * name
blanchet@43085
   381
blanchet@43085
   382
blanchet@43085
   383
(** Isabelle arities **)
blanchet@43085
   384
blanchet@43085
   385
datatype arity_literal =
blanchet@43085
   386
  TConsLit of name * name * name list |
blanchet@43085
   387
  TVarLit of name * name
blanchet@43085
   388
blanchet@43085
   389
fun gen_TVars 0 = []
blanchet@43093
   390
  | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
blanchet@43085
   391
blanchet@43263
   392
val type_class = the_single @{sort type}
blanchet@43263
   393
blanchet@43263
   394
fun add_packed_sort tvar =
blanchet@43263
   395
  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
blanchet@43085
   396
blanchet@43086
   397
type arity_clause =
blanchet@43086
   398
  {name: string,
blanchet@43086
   399
   prem_lits: arity_literal list,
blanchet@43086
   400
   concl_lits: arity_literal}
blanchet@43085
   401
blanchet@43085
   402
(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
blanchet@43085
   403
fun make_axiom_arity_clause (tcons, name, (cls, args)) =
blanchet@43085
   404
  let
blanchet@43085
   405
    val tvars = gen_TVars (length args)
blanchet@43085
   406
    val tvars_srts = ListPair.zip (tvars, args)
blanchet@43085
   407
  in
blanchet@43086
   408
    {name = name,
blanchet@43263
   409
     prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
blanchet@43086
   410
     concl_lits = TConsLit (`make_type_class cls,
blanchet@43086
   411
                            `make_fixed_type_const tcons,
blanchet@43086
   412
                            tvars ~~ tvars)}
blanchet@43085
   413
  end
blanchet@43085
   414
blanchet@43085
   415
fun arity_clause _ _ (_, []) = []
blanchet@43085
   416
  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
blanchet@43085
   417
      arity_clause seen n (tcons,ars)
blanchet@43085
   418
  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
blanchet@43085
   419
      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
blanchet@43085
   420
          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) ::
blanchet@43085
   421
          arity_clause seen (n+1) (tcons,ars)
blanchet@43085
   422
      else
blanchet@43085
   423
          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
blanchet@43085
   424
          arity_clause (class::seen) n (tcons,ars)
blanchet@43085
   425
blanchet@43085
   426
fun multi_arity_clause [] = []
blanchet@43085
   427
  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
blanchet@43085
   428
      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
blanchet@43085
   429
blanchet@43085
   430
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
blanchet@43085
   431
  provided its arguments have the corresponding sorts.*)
blanchet@43085
   432
fun type_class_pairs thy tycons classes =
blanchet@43093
   433
  let
blanchet@43093
   434
    val alg = Sign.classes_of thy
blanchet@43093
   435
    fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
blanchet@43093
   436
    fun add_class tycon class =
blanchet@43093
   437
      cons (class, domain_sorts tycon class)
blanchet@43093
   438
      handle Sorts.CLASS_ERROR _ => I
blanchet@43093
   439
    fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
blanchet@43093
   440
  in map try_classes tycons end
blanchet@43085
   441
blanchet@43085
   442
(*Proving one (tycon, class) membership may require proving others, so iterate.*)
blanchet@43085
   443
fun iter_type_class_pairs _ _ [] = ([], [])
blanchet@43085
   444
  | iter_type_class_pairs thy tycons classes =
blanchet@43263
   445
      let
blanchet@43263
   446
        fun maybe_insert_class s =
blanchet@43263
   447
          (s <> type_class andalso not (member (op =) classes s))
blanchet@43263
   448
          ? insert (op =) s
blanchet@43263
   449
        val cpairs = type_class_pairs thy tycons classes
blanchet@43263
   450
        val newclasses =
blanchet@43263
   451
          [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
blanchet@43263
   452
        val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
blanchet@43266
   453
      in (classes' @ classes, union (op =) cpairs' cpairs) end
blanchet@43085
   454
blanchet@43085
   455
fun make_arity_clauses thy tycons =
blanchet@43085
   456
  iter_type_class_pairs thy tycons ##> multi_arity_clause
blanchet@43085
   457
blanchet@43085
   458
blanchet@43085
   459
(** Isabelle class relations **)
blanchet@43085
   460
blanchet@43086
   461
type class_rel_clause =
blanchet@43086
   462
  {name: string,
blanchet@43086
   463
   subclass: name,
blanchet@43086
   464
   superclass: name}
blanchet@43085
   465
blanchet@43085
   466
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
blanchet@43085
   467
fun class_pairs _ [] _ = []
blanchet@43085
   468
  | class_pairs thy subs supers =
blanchet@43085
   469
      let
blanchet@43085
   470
        val class_less = Sorts.class_less (Sign.classes_of thy)
blanchet@43085
   471
        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
blanchet@43085
   472
        fun add_supers sub = fold (add_super sub) supers
blanchet@43085
   473
      in fold add_supers subs [] end
blanchet@43085
   474
blanchet@43085
   475
fun make_class_rel_clause (sub,super) =
blanchet@43086
   476
  {name = sub ^ "_" ^ super,
blanchet@43086
   477
   subclass = `make_type_class sub,
blanchet@43086
   478
   superclass = `make_type_class super}
blanchet@43085
   479
blanchet@43085
   480
fun make_class_rel_clauses thy subs supers =
blanchet@43093
   481
  map make_class_rel_clause (class_pairs thy subs supers)
blanchet@43085
   482
blanchet@43085
   483
datatype combterm =
blanchet@43085
   484
  CombConst of name * typ * typ list |
blanchet@43085
   485
  CombVar of name * typ |
blanchet@43085
   486
  CombApp of combterm * combterm
blanchet@43085
   487
blanchet@43085
   488
fun combtyp_of (CombConst (_, T, _)) = T
blanchet@43085
   489
  | combtyp_of (CombVar (_, T)) = T
blanchet@43085
   490
  | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
blanchet@43085
   491
blanchet@43085
   492
(*gets the head of a combinator application, along with the list of arguments*)
blanchet@43085
   493
fun strip_combterm_comb u =
blanchet@43085
   494
    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
blanchet@43085
   495
        |   stripc  x =  x
blanchet@43085
   496
    in stripc(u,[]) end
blanchet@43085
   497
blanchet@43085
   498
fun atyps_of T = fold_atyps (insert (op =)) T []
blanchet@43085
   499
blanchet@43085
   500
fun new_skolem_const_name s num_T_args =
blanchet@43085
   501
  [new_skolem_const_prefix, s, string_of_int num_T_args]
blanchet@43085
   502
  |> space_implode Long_Name.separator
blanchet@43085
   503
blanchet@43085
   504
(* Converts a term (with combinators) into a combterm. Also accumulates sort
blanchet@43085
   505
   infomation. *)
blanchet@43085
   506
fun combterm_from_term thy bs (P $ Q) =
blanchet@43085
   507
    let
blanchet@43085
   508
      val (P', P_atomics_Ts) = combterm_from_term thy bs P
blanchet@43085
   509
      val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
blanchet@43085
   510
    in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
blanchet@43085
   511
  | combterm_from_term thy _ (Const (c, T)) =
blanchet@43085
   512
    let
blanchet@43085
   513
      val tvar_list =
blanchet@43085
   514
        (if String.isPrefix old_skolem_const_prefix c then
blanchet@43085
   515
           [] |> Term.add_tvarsT T |> map TVar
blanchet@43085
   516
         else
blanchet@43085
   517
           (c, T) |> Sign.const_typargs thy)
blanchet@43085
   518
      val c' = CombConst (`make_fixed_const c, T, tvar_list)
blanchet@43085
   519
    in (c', atyps_of T) end
blanchet@43085
   520
  | combterm_from_term _ _ (Free (v, T)) =
blanchet@43085
   521
    (CombConst (`make_fixed_var v, T, []), atyps_of T)
blanchet@43085
   522
  | combterm_from_term _ _ (Var (v as (s, _), T)) =
blanchet@43085
   523
    (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
blanchet@43085
   524
       let
blanchet@43085
   525
         val Ts = T |> strip_type |> swap |> op ::
blanchet@43085
   526
         val s' = new_skolem_const_name s (length Ts)
blanchet@43085
   527
       in CombConst (`make_fixed_const s', T, Ts) end
blanchet@43085
   528
     else
blanchet@43085
   529
       CombVar ((make_schematic_var v, s), T), atyps_of T)
blanchet@43085
   530
  | combterm_from_term _ bs (Bound j) =
blanchet@43085
   531
    nth bs j
blanchet@43085
   532
    |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
blanchet@43085
   533
  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
blanchet@43085
   534
blanchet@43085
   535
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
blanchet@43085
   536
blanchet@43085
   537
(* (quasi-)underapproximation of the truth *)
blanchet@43085
   538
fun is_locality_global Local = false
blanchet@43085
   539
  | is_locality_global Assum = false
blanchet@43085
   540
  | is_locality_global Chained = false
blanchet@43085
   541
  | is_locality_global _ = true
blanchet@43085
   542
blanchet@42613
   543
datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
blanchet@42613
   544
datatype type_level =
blanchet@42613
   545
  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
blanchet@43128
   546
datatype type_heaviness = Heavyweight | Lightweight
blanchet@42613
   547
blanchet@43102
   548
datatype type_sys =
blanchet@42722
   549
  Simple_Types of type_level |
blanchet@42837
   550
  Preds of polymorphism * type_level * type_heaviness |
blanchet@42837
   551
  Tags of polymorphism * type_level * type_heaviness
blanchet@42613
   552
blanchet@42689
   553
fun try_unsuffixes ss s =
blanchet@42689
   554
  fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
blanchet@42689
   555
blanchet@42613
   556
fun type_sys_from_string s =
blanchet@42722
   557
  (case try (unprefix "poly_") s of
blanchet@42722
   558
     SOME s => (SOME Polymorphic, s)
blanchet@42613
   559
   | NONE =>
blanchet@42613
   560
     case try (unprefix "mono_") s of
blanchet@42722
   561
       SOME s => (SOME Monomorphic, s)
blanchet@42722
   562
     | NONE =>
blanchet@42722
   563
       case try (unprefix "mangled_") s of
blanchet@42722
   564
         SOME s => (SOME Mangled_Monomorphic, s)
blanchet@42722
   565
       | NONE => (NONE, s))
blanchet@42613
   566
  ||> (fn s =>
blanchet@42689
   567
          (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
blanchet@42689
   568
          case try_unsuffixes ["?", "_query"] s of
blanchet@42613
   569
            SOME s => (Nonmonotonic_Types, s)
blanchet@42613
   570
          | NONE =>
blanchet@42689
   571
            case try_unsuffixes ["!", "_bang"] s of
blanchet@42613
   572
              SOME s => (Finite_Types, s)
blanchet@42613
   573
            | NONE => (All_Types, s))
blanchet@42828
   574
  ||> apsnd (fn s =>
blanchet@42837
   575
                case try (unsuffix "_heavy") s of
blanchet@43128
   576
                  SOME s => (Heavyweight, s)
blanchet@43128
   577
                | NONE => (Lightweight, s))
blanchet@42837
   578
  |> (fn (poly, (level, (heaviness, core))) =>
blanchet@42837
   579
         case (core, (poly, level, heaviness)) of
blanchet@43128
   580
           ("simple", (NONE, _, Lightweight)) => Simple_Types level
blanchet@42854
   581
         | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
blanchet@42851
   582
         | ("tags", (SOME Polymorphic, All_Types, _)) =>
blanchet@42854
   583
           Tags (Polymorphic, All_Types, heaviness)
blanchet@42886
   584
         | ("tags", (SOME Polymorphic, _, _)) =>
blanchet@42886
   585
           (* The actual light encoding is very unsound. *)
blanchet@43128
   586
           Tags (Polymorphic, level, Heavyweight)
blanchet@42854
   587
         | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
blanchet@43128
   588
         | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
blanchet@43128
   589
           Preds (poly, Const_Arg_Types, Lightweight)
blanchet@43128
   590
         | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
blanchet@43128
   591
           Preds (Polymorphic, No_Types, Lightweight)
blanchet@42753
   592
         | _ => raise Same.SAME)
blanchet@42753
   593
  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
blanchet@42613
   594
blanchet@42722
   595
fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
blanchet@42828
   596
  | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
blanchet@42828
   597
  | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
blanchet@42613
   598
blanchet@42722
   599
fun level_of_type_sys (Simple_Types level) = level
blanchet@42828
   600
  | level_of_type_sys (Preds (_, level, _)) = level
blanchet@42828
   601
  | level_of_type_sys (Tags (_, level, _)) = level
blanchet@42828
   602
blanchet@43128
   603
fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
blanchet@42837
   604
  | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
blanchet@42837
   605
  | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
blanchet@42831
   606
blanchet@42687
   607
fun is_type_level_virtually_sound level =
blanchet@42687
   608
  level = All_Types orelse level = Nonmonotonic_Types
blanchet@42613
   609
val is_type_sys_virtually_sound =
blanchet@42613
   610
  is_type_level_virtually_sound o level_of_type_sys
blanchet@42613
   611
blanchet@42613
   612
fun is_type_level_fairly_sound level =
blanchet@42613
   613
  is_type_level_virtually_sound level orelse level = Finite_Types
blanchet@42613
   614
val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
blanchet@42613
   615
blanchet@42994
   616
fun is_setting_higher_order THF (Simple_Types _) = true
blanchet@42994
   617
  | is_setting_higher_order _ _ = false
blanchet@42994
   618
blanchet@43101
   619
fun choose_format formats (Simple_Types level) =
blanchet@43101
   620
    if member (op =) formats THF then (THF, Simple_Types level)
blanchet@43101
   621
    else if member (op =) formats TFF then (TFF, Simple_Types level)
blanchet@43128
   622
    else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
blanchet@43101
   623
  | choose_format formats type_sys =
blanchet@43101
   624
    (case hd formats of
blanchet@43101
   625
       CNF_UEQ =>
blanchet@43101
   626
       (CNF_UEQ, case type_sys of
blanchet@43101
   627
                   Preds stuff =>
blanchet@43289
   628
                   (if is_type_sys_fairly_sound type_sys then Tags else Preds)
blanchet@43101
   629
                       stuff
blanchet@43101
   630
                 | _ => type_sys)
blanchet@43101
   631
     | format => (format, type_sys))
blanchet@43101
   632
blanchet@40114
   633
type translated_formula =
blanchet@38752
   634
  {name: string,
blanchet@42640
   635
   locality: locality,
blanchet@42525
   636
   kind: formula_kind,
blanchet@42562
   637
   combformula: (name, typ, combterm) formula,
blanchet@42562
   638
   atomic_types: typ list}
blanchet@38282
   639
blanchet@42640
   640
fun update_combformula f ({name, locality, kind, combformula, atomic_types}
blanchet@42640
   641
                          : translated_formula) =
blanchet@42640
   642
  {name = name, locality = locality, kind = kind, combformula = f combformula,
blanchet@42562
   643
   atomic_types = atomic_types} : translated_formula
blanchet@42542
   644
blanchet@42558
   645
fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
blanchet@42558
   646
blanchet@43064
   647
val type_instance = Sign.typ_instance o Proof_Context.theory_of
blanchet@43064
   648
blanchet@43064
   649
fun insert_type ctxt get_T x xs =
blanchet@43064
   650
  let val T = get_T x in
blanchet@43064
   651
    if exists (curry (type_instance ctxt) T o get_T) xs then xs
blanchet@43064
   652
    else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
blanchet@43064
   653
  end
blanchet@42677
   654
blanchet@42753
   655
(* The Booleans indicate whether all type arguments should be kept. *)
blanchet@42753
   656
datatype type_arg_policy =
blanchet@42753
   657
  Explicit_Type_Args of bool |
blanchet@42753
   658
  Mangled_Type_Args of bool |
blanchet@42753
   659
  No_Type_Args
blanchet@41136
   660
blanchet@42836
   661
fun should_drop_arg_type_args (Simple_Types _) =
blanchet@42836
   662
    false (* since TFF doesn't support overloading *)
blanchet@42836
   663
  | should_drop_arg_type_args type_sys =
blanchet@42836
   664
    level_of_type_sys type_sys = All_Types andalso
blanchet@43128
   665
    heaviness_of_type_sys type_sys = Heavyweight
blanchet@42831
   666
blanchet@43128
   667
fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
blanchet@43105
   668
  | general_type_arg_policy type_sys =
blanchet@43105
   669
    if level_of_type_sys type_sys = No_Types then
blanchet@43105
   670
      No_Type_Args
blanchet@43105
   671
    else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
blanchet@43105
   672
      Mangled_Type_Args (should_drop_arg_type_args type_sys)
blanchet@43105
   673
    else
blanchet@43105
   674
      Explicit_Type_Args (should_drop_arg_type_args type_sys)
blanchet@42563
   675
blanchet@42951
   676
fun type_arg_policy type_sys s =
blanchet@42951
   677
  if s = @{const_name HOL.eq} orelse
blanchet@42966
   678
     (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
blanchet@42951
   679
    No_Type_Args
blanchet@43105
   680
  else if s = type_tag_name then
blanchet@43105
   681
    Explicit_Type_Args false
blanchet@42951
   682
  else
blanchet@42951
   683
    general_type_arg_policy type_sys
blanchet@42227
   684
blanchet@43085
   685
(*Make literals for sorted type variables*)
blanchet@43263
   686
fun generic_add_sorts_on_type (_, []) = I
blanchet@43263
   687
  | generic_add_sorts_on_type ((x, i), s :: ss) =
blanchet@43263
   688
    generic_add_sorts_on_type ((x, i), ss)
blanchet@43263
   689
    #> (if s = the_single @{sort HOL.type} then
blanchet@43093
   690
          I
blanchet@43093
   691
        else if i = ~1 then
blanchet@43263
   692
          insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
blanchet@43093
   693
        else
blanchet@43263
   694
          insert (op =) (TyLitVar (`make_type_class s,
blanchet@43263
   695
                                   (make_schematic_type_var (x, i), x))))
blanchet@43263
   696
fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
blanchet@43263
   697
  | add_sorts_on_tfree _ = I
blanchet@43263
   698
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
blanchet@43263
   699
  | add_sorts_on_tvar _ = I
blanchet@43085
   700
blanchet@43263
   701
fun type_literals_for_types type_sys add_sorts_on_typ Ts =
blanchet@43263
   702
  [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
blanchet@41137
   703
blanchet@42534
   704
fun mk_aconns c phis =
blanchet@42534
   705
  let val (phis', phi') = split_last phis in
blanchet@42534
   706
    fold_rev (mk_aconn c) phis' phi'
blanchet@42534
   707
  end
blanchet@38282
   708
fun mk_ahorn [] phi = phi
blanchet@42534
   709
  | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
blanchet@42522
   710
fun mk_aquant _ [] phi = phi
blanchet@42522
   711
  | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
blanchet@42522
   712
    if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
blanchet@42522
   713
  | mk_aquant q xs phi = AQuant (q, xs, phi)
blanchet@38282
   714
blanchet@42522
   715
fun close_universally atom_vars phi =
blanchet@41145
   716
  let
blanchet@41145
   717
    fun formula_vars bounds (AQuant (_, xs, phi)) =
blanchet@42526
   718
        formula_vars (map fst xs @ bounds) phi
blanchet@41145
   719
      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
blanchet@42522
   720
      | formula_vars bounds (AAtom tm) =
blanchet@42526
   721
        union (op =) (atom_vars tm []
blanchet@42526
   722
                      |> filter_out (member (op =) bounds o fst))
blanchet@42522
   723
  in mk_aquant AForall (formula_vars [] phi []) phi end
blanchet@42522
   724
blanchet@42531
   725
fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
blanchet@42522
   726
  | combterm_vars (CombConst _) = I
blanchet@42574
   727
  | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
blanchet@42674
   728
fun close_combformula_universally phi = close_universally combterm_vars phi
blanchet@42522
   729
blanchet@42522
   730
fun term_vars (ATerm (name as (s, _), tms)) =
blanchet@42998
   731
  is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
blanchet@42674
   732
fun close_formula_universally phi = close_universally term_vars phi
blanchet@41145
   733
blanchet@42994
   734
val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
blanchet@42994
   735
val homo_infinite_type = Type (homo_infinite_type_name, [])
blanchet@42994
   736
blanchet@43178
   737
fun fo_term_from_typ format type_sys =
blanchet@42994
   738
  let
blanchet@42994
   739
    fun term (Type (s, Ts)) =
blanchet@43178
   740
      ATerm (case (is_setting_higher_order format type_sys, s) of
blanchet@42994
   741
               (true, @{type_name bool}) => `I tptp_bool_type
blanchet@42994
   742
             | (true, @{type_name fun}) => `I tptp_fun_type
blanchet@43178
   743
             | _ => if s = homo_infinite_type_name andalso
blanchet@43178
   744
                       (format = TFF orelse format = THF) then
blanchet@43178
   745
                      `I tptp_individual_type
blanchet@43178
   746
                    else
blanchet@43178
   747
                      `make_fixed_type_const s,
blanchet@42994
   748
             map term Ts)
blanchet@42994
   749
    | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
blanchet@42994
   750
    | term (TVar ((x as (s, _)), _)) =
blanchet@42994
   751
      ATerm ((make_schematic_type_var x, s), [])
blanchet@42994
   752
  in term end
blanchet@42562
   753
blanchet@42562
   754
(* This shouldn't clash with anything else. *)
blanchet@42542
   755
val mangled_type_sep = "\000"
blanchet@42542
   756
blanchet@42562
   757
fun generic_mangled_type_name f (ATerm (name, [])) = f name
blanchet@42562
   758
  | generic_mangled_type_name f (ATerm (name, tys)) =
blanchet@42761
   759
    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
blanchet@42761
   760
    ^ ")"
blanchet@42542
   761
blanchet@42998
   762
val bool_atype = AType (`I tptp_bool_type)
blanchet@42998
   763
blanchet@43085
   764
fun make_simple_type s =
blanchet@43085
   765
  if s = tptp_bool_type orelse s = tptp_fun_type orelse
blanchet@43085
   766
     s = tptp_individual_type then
blanchet@43085
   767
    s
blanchet@43085
   768
  else
blanchet@43085
   769
    simple_type_prefix ^ ascii_of s
blanchet@43085
   770
blanchet@43178
   771
fun ho_type_from_fo_term format type_sys pred_sym ary =
blanchet@42963
   772
  let
blanchet@42963
   773
    fun to_atype ty =
blanchet@42963
   774
      AType ((make_simple_type (generic_mangled_type_name fst ty),
blanchet@42963
   775
              generic_mangled_type_name snd ty))
blanchet@42963
   776
    fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
blanchet@42998
   777
    fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
blanchet@42994
   778
      | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
blanchet@42994
   779
    fun to_ho (ty as ATerm ((s, _), tys)) =
blanchet@42994
   780
      if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
blanchet@43178
   781
  in if is_setting_higher_order format type_sys then to_ho else to_fo ary end
blanchet@42963
   782
blanchet@43178
   783
fun mangled_type format type_sys pred_sym ary =
blanchet@43178
   784
  ho_type_from_fo_term format type_sys pred_sym ary
blanchet@43178
   785
  o fo_term_from_typ format type_sys
blanchet@42963
   786
blanchet@43178
   787
fun mangled_const_name format type_sys T_args (s, s') =
blanchet@42963
   788
  let
blanchet@43178
   789
    val ty_args = map (fo_term_from_typ format type_sys) T_args
blanchet@42963
   790
    fun type_suffix f g =
blanchet@42963
   791
      fold_rev (curry (op ^) o g o prefix mangled_type_sep
blanchet@42963
   792
                o generic_mangled_type_name f) ty_args ""
blanchet@42963
   793
  in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
blanchet@42542
   794
blanchet@42542
   795
val parse_mangled_ident =
blanchet@42542
   796
  Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
blanchet@42542
   797
blanchet@42542
   798
fun parse_mangled_type x =
blanchet@42542
   799
  (parse_mangled_ident
blanchet@42542
   800
   -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
blanchet@42542
   801
                    [] >> ATerm) x
blanchet@42542
   802
and parse_mangled_types x =
blanchet@42542
   803
  (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
blanchet@42542
   804
blanchet@42542
   805
fun unmangled_type s =
blanchet@42542
   806
  s |> suffix ")" |> raw_explode
blanchet@42542
   807
    |> Scan.finite Symbol.stopper
blanchet@42542
   808
           (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
blanchet@42542
   809
                                                quote s)) parse_mangled_type))
blanchet@42542
   810
    |> fst
blanchet@42542
   811
blanchet@42561
   812
val unmangled_const_name = space_explode mangled_type_sep #> hd
blanchet@42542
   813
fun unmangled_const s =
blanchet@42542
   814
  let val ss = space_explode mangled_type_sep s in
blanchet@42542
   815
    (hd ss, map unmangled_type (tl ss))
blanchet@42542
   816
  end
blanchet@42542
   817
blanchet@43017
   818
fun introduce_proxies format type_sys =
blanchet@42568
   819
  let
blanchet@43017
   820
    fun intro top_level (CombApp (tm1, tm2)) =
blanchet@43017
   821
        CombApp (intro top_level tm1, intro false tm2)
blanchet@43017
   822
      | intro top_level (CombConst (name as (s, _), T, T_args)) =
blanchet@42570
   823
        (case proxify_const s of
blanchet@43159
   824
           SOME proxy_base =>
blanchet@43000
   825
           if top_level orelse is_setting_higher_order format type_sys then
blanchet@43000
   826
             case (top_level, s) of
blanchet@43000
   827
               (_, "c_False") => (`I tptp_false, [])
blanchet@43000
   828
             | (_, "c_True") => (`I tptp_true, [])
blanchet@43000
   829
             | (false, "c_Not") => (`I tptp_not, [])
blanchet@43000
   830
             | (false, "c_conj") => (`I tptp_and, [])
blanchet@43000
   831
             | (false, "c_disj") => (`I tptp_or, [])
blanchet@43000
   832
             | (false, "c_implies") => (`I tptp_implies, [])
blanchet@43000
   833
             | (false, s) =>
blanchet@43017
   834
               if is_tptp_equal s then (`I tptp_equal, [])
blanchet@43017
   835
               else (proxy_base |>> prefix const_prefix, T_args)
blanchet@43000
   836
             | _ => (name, [])
blanchet@42569
   837
           else
blanchet@42574
   838
             (proxy_base |>> prefix const_prefix, T_args)
blanchet@42574
   839
          | NONE => (name, T_args))
blanchet@42574
   840
        |> (fn (name, T_args) => CombConst (name, T, T_args))
blanchet@43017
   841
      | intro _ tm = tm
blanchet@43017
   842
  in intro true end
blanchet@42568
   843
blanchet@42994
   844
fun combformula_from_prop thy format type_sys eq_as_iff =
blanchet@38282
   845
  let
blanchet@42568
   846
    fun do_term bs t atomic_types =
blanchet@41140
   847
      combterm_from_term thy bs (Envir.eta_contract t)
blanchet@42994
   848
      |>> (introduce_proxies format type_sys #> AAtom)
blanchet@42568
   849
      ||> union (op =) atomic_types
blanchet@38282
   850
    fun do_quant bs q s T t' =
blanchet@38518
   851
      let val s = Name.variant (map fst bs) s in
blanchet@38518
   852
        do_formula ((s, T) :: bs) t'
blanchet@42562
   853
        #>> mk_aquant q [(`make_bound_var s, SOME T)]
blanchet@38518
   854
      end
blanchet@38282
   855
    and do_conn bs c t1 t2 =
blanchet@43198
   856
      do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
blanchet@38282
   857
    and do_formula bs t =
blanchet@38282
   858
      case t of
blanchet@43096
   859
        @{const Trueprop} $ t1 => do_formula bs t1
blanchet@43096
   860
      | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
blanchet@38282
   861
      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
blanchet@38282
   862
        do_quant bs AForall s T t'
blanchet@38282
   863
      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
blanchet@38282
   864
        do_quant bs AExists s T t'
haftmann@38795
   865
      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
haftmann@38795
   866
      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
haftmann@38786
   867
      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
haftmann@38864
   868
      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
blanchet@41140
   869
        if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
blanchet@41140
   870
      | _ => do_term bs t
blanchet@38282
   871
  in do_formula [] end
blanchet@38282
   872
blanchet@43264
   873
fun presimplify_term _ [] t = t
blanchet@43264
   874
  | presimplify_term ctxt presimp_consts t =
blanchet@43264
   875
    t |> exists_Const (member (op =) presimp_consts o fst) t
blanchet@43264
   876
         ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
blanchet@43264
   877
            #> Meson.presimplify ctxt
blanchet@43264
   878
            #> prop_of)
blanchet@38282
   879
wenzelm@41491
   880
fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
blanchet@38282
   881
fun conceal_bounds Ts t =
blanchet@38282
   882
  subst_bounds (map (Free o apfst concealed_bound_name)
blanchet@38282
   883
                    (0 upto length Ts - 1 ~~ Ts), t)
blanchet@38282
   884
fun reveal_bounds Ts =
blanchet@38282
   885
  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
blanchet@38282
   886
                    (0 upto length Ts - 1 ~~ Ts))
blanchet@38282
   887
blanchet@43265
   888
fun is_fun_equality (@{const_name HOL.eq},
blanchet@43265
   889
                     Type (_, [Type (@{type_name fun}, _), _])) = true
blanchet@43265
   890
  | is_fun_equality _ = false
blanchet@43265
   891
blanchet@42747
   892
fun extensionalize_term ctxt t =
blanchet@43265
   893
  if exists_Const is_fun_equality t then
blanchet@43265
   894
    let val thy = Proof_Context.theory_of ctxt in
blanchet@43265
   895
      t |> cterm_of thy |> Meson.extensionalize_conv ctxt
blanchet@43265
   896
        |> prop_of |> Logic.dest_equals |> snd
blanchet@43265
   897
    end
blanchet@43265
   898
  else
blanchet@43265
   899
    t
blanchet@38608
   900
blanchet@38282
   901
fun introduce_combinators_in_term ctxt kind t =
wenzelm@42361
   902
  let val thy = Proof_Context.theory_of ctxt in
blanchet@38491
   903
    if Meson.is_fol_term thy t then
blanchet@38491
   904
      t
blanchet@38491
   905
    else
blanchet@38491
   906
      let
blanchet@38491
   907
        fun aux Ts t =
blanchet@38491
   908
          case t of
blanchet@38491
   909
            @{const Not} $ t1 => @{const Not} $ aux Ts t1
blanchet@38491
   910
          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
blanchet@38491
   911
            t0 $ Abs (s, T, aux (T :: Ts) t')
blanchet@38652
   912
          | (t0 as Const (@{const_name All}, _)) $ t1 =>
blanchet@38652
   913
            aux Ts (t0 $ eta_expand Ts t1 1)
blanchet@38491
   914
          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
blanchet@38491
   915
            t0 $ Abs (s, T, aux (T :: Ts) t')
blanchet@38652
   916
          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
blanchet@38652
   917
            aux Ts (t0 $ eta_expand Ts t1 1)
haftmann@38795
   918
          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
haftmann@38795
   919
          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
haftmann@38786
   920
          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
haftmann@38864
   921
          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
blanchet@38491
   922
              $ t1 $ t2 =>
blanchet@38491
   923
            t0 $ aux Ts t1 $ aux Ts t2
blanchet@38491
   924
          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
blanchet@38491
   925
                   t
blanchet@38491
   926
                 else
blanchet@38491
   927
                   t |> conceal_bounds Ts
blanchet@38491
   928
                     |> Envir.eta_contract
blanchet@38491
   929
                     |> cterm_of thy
blanchet@39890
   930
                     |> Meson_Clausify.introduce_combinators_in_cterm
blanchet@38491
   931
                     |> prop_of |> Logic.dest_equals |> snd
blanchet@38491
   932
                     |> reveal_bounds Ts
blanchet@39370
   933
        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
blanchet@38491
   934
      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
blanchet@38491
   935
      handle THM _ =>
blanchet@38491
   936
             (* A type variable of sort "{}" will make abstraction fail. *)
blanchet@38613
   937
             if kind = Conjecture then HOLogic.false_const
blanchet@38613
   938
             else HOLogic.true_const
blanchet@38491
   939
  end
blanchet@38282
   940
blanchet@38282
   941
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
blanchet@42353
   942
   same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
blanchet@38282
   943
fun freeze_term t =
blanchet@38282
   944
  let
blanchet@38282
   945
    fun aux (t $ u) = aux t $ aux u
blanchet@38282
   946
      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
blanchet@38282
   947
      | aux (Var ((s, i), T)) =
blanchet@38282
   948
        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
blanchet@38282
   949
      | aux t = t
blanchet@38282
   950
  in t |> exists_subterm is_Var t ? aux end
blanchet@38282
   951
blanchet@43264
   952
fun preprocess_prop ctxt presimp_consts kind t =
blanchet@38282
   953
  let
wenzelm@42361
   954
    val thy = Proof_Context.theory_of ctxt
blanchet@38608
   955
    val t = t |> Envir.beta_eta_contract
blanchet@42944
   956
              |> transform_elim_prop
blanchet@41211
   957
              |> Object_Logic.atomize_term thy
blanchet@42563
   958
    val need_trueprop = (fastype_of t = @{typ bool})
blanchet@43096
   959
  in
blanchet@43096
   960
    t |> need_trueprop ? HOLogic.mk_Trueprop
blanchet@43096
   961
      |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
blanchet@43096
   962
      |> extensionalize_term ctxt
blanchet@43264
   963
      |> presimplify_term ctxt presimp_consts
blanchet@43120
   964
      |> perhaps (try (HOLogic.dest_Trueprop))
blanchet@43096
   965
      |> introduce_combinators_in_term ctxt kind
blanchet@43096
   966
  end
blanchet@43096
   967
blanchet@43096
   968
(* making fact and conjecture formulas *)
blanchet@43096
   969
fun make_formula thy format type_sys eq_as_iff name loc kind t =
blanchet@43096
   970
  let
blanchet@42962
   971
    val (combformula, atomic_types) =
blanchet@42994
   972
      combformula_from_prop thy format type_sys eq_as_iff t []
blanchet@38282
   973
  in
blanchet@42640
   974
    {name = name, locality = loc, kind = kind, combformula = combformula,
blanchet@42562
   975
     atomic_types = atomic_types}
blanchet@38282
   976
  end
blanchet@38282
   977
blanchet@43264
   978
fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp_consts
blanchet@42994
   979
              ((name, loc), t) =
blanchet@43096
   980
  let val thy = Proof_Context.theory_of ctxt in
blanchet@43096
   981
    case (keep_trivial,
blanchet@43264
   982
          t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
blanchet@43096
   983
            |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
blanchet@43096
   984
      (false,
blanchet@43096
   985
       formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
blanchet@43096
   986
      if s = tptp_true then NONE else SOME formula
blanchet@43096
   987
    | (_, formula) => SOME formula
blanchet@43096
   988
  end
blanchet@42561
   989
blanchet@43264
   990
fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
blanchet@43096
   991
  let
blanchet@43096
   992
    val thy = Proof_Context.theory_of ctxt
blanchet@43096
   993
    val last = length ts - 1
blanchet@43096
   994
  in
blanchet@42709
   995
    map2 (fn j => fn t =>
blanchet@42709
   996
             let
blanchet@42709
   997
               val (kind, maybe_negate) =
blanchet@42709
   998
                 if j = last then
blanchet@42709
   999
                   (Conjecture, I)
blanchet@42709
  1000
                 else
blanchet@42709
  1001
                   (prem_kind,
blanchet@42709
  1002
                    if prem_kind = Conjecture then update_combformula mk_anot
blanchet@42709
  1003
                    else I)
blanchet@42709
  1004
              in
blanchet@43264
  1005
                t |> preproc ?
blanchet@43264
  1006
                     (preprocess_prop ctxt presimp_consts kind #> freeze_term)
blanchet@43193
  1007
                  |> make_formula thy format type_sys (format <> CNF)
blanchet@43293
  1008
                                  (string_of_int j) Local kind
blanchet@42962
  1009
                  |> maybe_negate
blanchet@42709
  1010
              end)
blanchet@38613
  1011
         (0 upto last) ts
blanchet@38613
  1012
  end
blanchet@38282
  1013
blanchet@42682
  1014
(** Finite and infinite type inference **)
blanchet@42682
  1015
blanchet@42886
  1016
fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
blanchet@42886
  1017
  | deep_freeze_atyp T = T
blanchet@42886
  1018
val deep_freeze_type = map_atyps deep_freeze_atyp
blanchet@42886
  1019
blanchet@42682
  1020
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
blanchet@42682
  1021
   dangerous because their "exhaust" properties can easily lead to unsound ATP
blanchet@42682
  1022
   proofs. On the other hand, all HOL infinite types can be given the same
blanchet@42682
  1023
   models in first-order logic (via Löwenheim-Skolem). *)
blanchet@42682
  1024
blanchet@42886
  1025
fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
blanchet@42886
  1026
    exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
blanchet@42836
  1027
  | should_encode_type _ _ All_Types _ = true
blanchet@42682
  1028
  | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
blanchet@42682
  1029
  | should_encode_type _ _ _ _ = false
blanchet@42682
  1030
blanchet@42837
  1031
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
blanchet@42834
  1032
                             should_predicate_on_var T =
blanchet@43128
  1033
    (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
blanchet@42878
  1034
    should_encode_type ctxt nonmono_Ts level T
blanchet@42834
  1035
  | should_predicate_on_type _ _ _ _ _ = false
blanchet@42682
  1036
blanchet@42836
  1037
fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
blanchet@42836
  1038
    String.isPrefix bound_var_prefix s
blanchet@42836
  1039
  | is_var_or_bound_var (CombVar _) = true
blanchet@42836
  1040
  | is_var_or_bound_var _ = false
blanchet@42836
  1041
blanchet@42829
  1042
datatype tag_site = Top_Level | Eq_Arg | Elsewhere
blanchet@42829
  1043
blanchet@42829
  1044
fun should_tag_with_type _ _ _ Top_Level _ _ = false
blanchet@42837
  1045
  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
blanchet@42837
  1046
    (case heaviness of
blanchet@43128
  1047
       Heavyweight => should_encode_type ctxt nonmono_Ts level T
blanchet@43128
  1048
     | Lightweight =>
blanchet@42836
  1049
       case (site, is_var_or_bound_var u) of
blanchet@42836
  1050
         (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
blanchet@42829
  1051
       | _ => false)
blanchet@42829
  1052
  | should_tag_with_type _ _ _ _ _ _ = false
blanchet@42682
  1053
blanchet@42994
  1054
fun homogenized_type ctxt nonmono_Ts level =
blanchet@42994
  1055
  let
blanchet@42994
  1056
    val should_encode = should_encode_type ctxt nonmono_Ts level
blanchet@42994
  1057
    fun homo 0 T = if should_encode T then T else homo_infinite_type
blanchet@42994
  1058
      | homo ary (Type (@{type_name fun}, [T1, T2])) =
blanchet@42994
  1059
        homo 0 T1 --> homo (ary - 1) T2
blanchet@42994
  1060
      | homo _ _ = raise Fail "expected function type"
blanchet@42994
  1061
  in homo end
blanchet@42682
  1062
blanchet@42573
  1063
(** "hBOOL" and "hAPP" **)
blanchet@41313
  1064
blanchet@42574
  1065
type sym_info =
blanchet@43064
  1066
  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
blanchet@42563
  1067
blanchet@43064
  1068
fun add_combterm_syms_to_table ctxt explicit_apply =
blanchet@42558
  1069
  let
blanchet@43064
  1070
    fun consider_var_arity const_T var_T max_ary =
blanchet@43064
  1071
      let
blanchet@43064
  1072
        fun iter ary T =
blanchet@43210
  1073
          if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
blanchet@43210
  1074
             type_instance ctxt (T, var_T) then
blanchet@43210
  1075
            ary
blanchet@43210
  1076
          else
blanchet@43210
  1077
            iter (ary + 1) (range_type T)
blanchet@43064
  1078
      in iter 0 const_T end
blanchet@43201
  1079
    fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
blanchet@43201
  1080
      if explicit_apply = NONE andalso
blanchet@43201
  1081
         (can dest_funT T orelse T = @{typ bool}) then
blanchet@43201
  1082
        let
blanchet@43201
  1083
          val bool_vars' = bool_vars orelse body_type T = @{typ bool}
blanchet@43201
  1084
          fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
blanchet@43201
  1085
            {pred_sym = pred_sym andalso not bool_vars',
blanchet@43213
  1086
             min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
blanchet@43201
  1087
             max_ary = max_ary, types = types}
blanchet@43201
  1088
          val fun_var_Ts' =
blanchet@43201
  1089
            fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
blanchet@43201
  1090
        in
blanchet@43201
  1091
          if bool_vars' = bool_vars andalso
blanchet@43201
  1092
             pointer_eq (fun_var_Ts', fun_var_Ts) then
blanchet@43201
  1093
            accum
blanchet@43167
  1094
          else
blanchet@43213
  1095
            ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
blanchet@43201
  1096
        end
blanchet@43201
  1097
      else
blanchet@43201
  1098
        accum
blanchet@43201
  1099
    fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
blanchet@43201
  1100
      let val (head, args) = strip_combterm_comb tm in
blanchet@42558
  1101
        (case head of
blanchet@42563
  1102
           CombConst ((s, _), T, _) =>
blanchet@42558
  1103
           if String.isPrefix bound_var_prefix s then
blanchet@43201
  1104
             add_var_or_bound_var T accum
blanchet@42558
  1105
           else
blanchet@43139
  1106
             let val ary = length args in
blanchet@43201
  1107
               ((bool_vars, fun_var_Ts),
blanchet@43064
  1108
                case Symtab.lookup sym_tab s of
blanchet@43064
  1109
                  SOME {pred_sym, min_ary, max_ary, types} =>
blanchet@43064
  1110
                  let
blanchet@43201
  1111
                    val pred_sym =
blanchet@43201
  1112
                      pred_sym andalso top_level andalso not bool_vars
blanchet@43064
  1113
                    val types' = types |> insert_type ctxt I T
blanchet@43064
  1114
                    val min_ary =
blanchet@43064
  1115
                      if is_some explicit_apply orelse
blanchet@43064
  1116
                         pointer_eq (types', types) then
blanchet@43064
  1117
                        min_ary
blanchet@43064
  1118
                      else
blanchet@43201
  1119
                        fold (consider_var_arity T) fun_var_Ts min_ary
blanchet@43064
  1120
                  in
blanchet@43201
  1121
                    Symtab.update (s, {pred_sym = pred_sym,
blanchet@43064
  1122
                                       min_ary = Int.min (ary, min_ary),
blanchet@43064
  1123
                                       max_ary = Int.max (ary, max_ary),
blanchet@43064
  1124
                                       types = types'})
blanchet@43064
  1125
                                  sym_tab
blanchet@43064
  1126
                  end
blanchet@43064
  1127
                | NONE =>
blanchet@43064
  1128
                  let
blanchet@43201
  1129
                    val pred_sym = top_level andalso not bool_vars
blanchet@43064
  1130
                    val min_ary =
blanchet@43064
  1131
                      case explicit_apply of
blanchet@43064
  1132
                        SOME true => 0
blanchet@43064
  1133
                      | SOME false => ary
blanchet@43201
  1134
                      | NONE => fold (consider_var_arity T) fun_var_Ts ary
blanchet@43064
  1135
                  in
blanchet@43201
  1136
                    Symtab.update_new (s, {pred_sym = pred_sym,
blanchet@43064
  1137
                                           min_ary = min_ary, max_ary = ary,
blanchet@43064
  1138
                                           types = [T]})
blanchet@43064
  1139
                                      sym_tab
blanchet@43064
  1140
                  end)
blanchet@43064
  1141
             end
blanchet@43201
  1142
         | CombVar (_, T) => add_var_or_bound_var T accum
blanchet@43064
  1143
         | _ => accum)
blanchet@43064
  1144
        |> fold (add false) args
blanchet@42558
  1145
      end
blanchet@43064
  1146
  in add true end
blanchet@43064
  1147
fun add_fact_syms_to_table ctxt explicit_apply =
blanchet@43064
  1148
  fact_lift (formula_fold NONE
blanchet@43064
  1149
                          (K (add_combterm_syms_to_table ctxt explicit_apply)))
blanchet@38282
  1150
blanchet@43139
  1151
val default_sym_tab_entries : (string * sym_info) list =
blanchet@43174
  1152
  (prefixed_predicator_name,
blanchet@43139
  1153
   {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
blanchet@42568
  1154
  ([tptp_false, tptp_true]
blanchet@43139
  1155
   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
blanchet@43139
  1156
  ([tptp_equal, tptp_old_equal]
blanchet@43139
  1157
   |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
blanchet@41140
  1158
blanchet@43064
  1159
fun sym_table_for_facts ctxt explicit_apply facts =
blanchet@43201
  1160
  ((false, []), Symtab.empty)
blanchet@43201
  1161
  |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
blanchet@43139
  1162
  |> fold Symtab.update default_sym_tab_entries
blanchet@38282
  1163
blanchet@42558
  1164
fun min_arity_of sym_tab s =
blanchet@42558
  1165
  case Symtab.lookup sym_tab s of
blanchet@42574
  1166
    SOME ({min_ary, ...} : sym_info) => min_ary
blanchet@42558
  1167
  | NONE =>
blanchet@42558
  1168
    case strip_prefix_and_unascii const_prefix s of
blanchet@42547
  1169
      SOME s =>
blanchet@42570
  1170
      let val s = s |> unmangled_const_name |> invert_const in
blanchet@42966
  1171
        if s = predicator_name then 1
blanchet@42966
  1172
        else if s = app_op_name then 2
blanchet@42966
  1173
        else if s = type_pred_name then 1
blanchet@42557
  1174
        else 0
blanchet@42547
  1175
      end
blanchet@42544
  1176
    | NONE => 0
blanchet@38282
  1177
blanchet@38282
  1178
(* True if the constant ever appears outside of the top-level position in
blanchet@38282
  1179
   literals, or if it appears with different arities (e.g., because of different
blanchet@38282
  1180
   type instantiations). If false, the constant always receives all of its
blanchet@38282
  1181
   arguments and is used as a predicate. *)
blanchet@42558
  1182
fun is_pred_sym sym_tab s =
blanchet@42558
  1183
  case Symtab.lookup sym_tab s of
blanchet@42574
  1184
    SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
blanchet@42574
  1185
    pred_sym andalso min_ary = max_ary
blanchet@42558
  1186
  | NONE => false
blanchet@38282
  1187
blanchet@42568
  1188
val predicator_combconst =
blanchet@42966
  1189
  CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
blanchet@42568
  1190
fun predicator tm = CombApp (predicator_combconst, tm)
blanchet@42542
  1191
blanchet@42568
  1192
fun introduce_predicators_in_combterm sym_tab tm =
blanchet@42542
  1193
  case strip_combterm_comb tm of
blanchet@42542
  1194
    (CombConst ((s, _), _, _), _) =>
blanchet@42568
  1195
    if is_pred_sym sym_tab s then tm else predicator tm
blanchet@42568
  1196
  | _ => predicator tm
blanchet@42542
  1197
blanchet@42544
  1198
fun list_app head args = fold (curry (CombApp o swap)) args head
blanchet@42544
  1199
blanchet@43130
  1200
val app_op = `make_fixed_const app_op_name
blanchet@43130
  1201
blanchet@42544
  1202
fun explicit_app arg head =
blanchet@42544
  1203
  let
blanchet@42562
  1204
    val head_T = combtyp_of head
blanchet@42693
  1205
    val (arg_T, res_T) = dest_funT head_T
blanchet@42544
  1206
    val explicit_app =
blanchet@43130
  1207
      CombConst (app_op, head_T --> head_T, [arg_T, res_T])
blanchet@42544
  1208
  in list_app explicit_app [head, arg] end
blanchet@42544
  1209
fun list_explicit_app head args = fold explicit_app args head
blanchet@38282
  1210
blanchet@42565
  1211
fun introduce_explicit_apps_in_combterm sym_tab =
blanchet@42544
  1212
  let
blanchet@42544
  1213
    fun aux tm =
blanchet@42544
  1214
      case strip_combterm_comb tm of
blanchet@42544
  1215
        (head as CombConst ((s, _), _, _), args) =>
blanchet@42544
  1216
        args |> map aux
blanchet@42557
  1217
             |> chop (min_arity_of sym_tab s)
blanchet@42544
  1218
             |>> list_app head
blanchet@42544
  1219
             |-> list_explicit_app
blanchet@42544
  1220
      | (head, args) => list_explicit_app head (map aux args)
blanchet@42544
  1221
  in aux end
blanchet@38282
  1222
blanchet@42753
  1223
fun chop_fun 0 T = ([], T)
blanchet@42753
  1224
  | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
blanchet@42753
  1225
    chop_fun (n - 1) ran_T |>> cons dom_T
blanchet@42753
  1226
  | chop_fun _ _ = raise Fail "unexpected non-function"
blanchet@42753
  1227
blanchet@42780
  1228
fun filter_type_args _ _ _ [] = []
blanchet@42780
  1229
  | filter_type_args thy s arity T_args =
blanchet@42834
  1230
    let
blanchet@42834
  1231
      (* will throw "TYPE" for pseudo-constants *)
blanchet@42966
  1232
      val U = if s = app_op_name then
blanchet@42834
  1233
                @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
blanchet@42834
  1234
              else
blanchet@42834
  1235
                s |> Sign.the_const_type thy
blanchet@42834
  1236
    in
blanchet@42781
  1237
      case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
blanchet@42781
  1238
        [] => []
blanchet@42781
  1239
      | res_U_vars =>
blanchet@42781
  1240
        let val U_args = (s, U) |> Sign.const_typargs thy in
blanchet@42781
  1241
          U_args ~~ T_args
blanchet@42781
  1242
          |> map_filter (fn (U, T) =>
blanchet@42781
  1243
                            if member (op =) res_U_vars (dest_TVar U) then
blanchet@42781
  1244
                              SOME T
blanchet@42781
  1245
                            else
blanchet@42781
  1246
                              NONE)
blanchet@42781
  1247
        end
blanchet@42780
  1248
    end
blanchet@42780
  1249
    handle TYPE _ => T_args
blanchet@42753
  1250
blanchet@43179
  1251
fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
blanchet@42753
  1252
  let
blanchet@42753
  1253
    val thy = Proof_Context.theory_of ctxt
blanchet@42753
  1254
    fun aux arity (CombApp (tm1, tm2)) =
blanchet@42753
  1255
        CombApp (aux (arity + 1) tm1, aux 0 tm2)
blanchet@42753
  1256
      | aux arity (CombConst (name as (s, _), T, T_args)) =
blanchet@43179
  1257
        (case strip_prefix_and_unascii const_prefix s of
blanchet@43179
  1258
           NONE => (name, T_args)
blanchet@43179
  1259
         | SOME s'' =>
blanchet@43179
  1260
           let
blanchet@43179
  1261
             val s'' = invert_const s''
blanchet@43179
  1262
             fun filtered_T_args false = T_args
blanchet@43179
  1263
               | filtered_T_args true = filter_type_args thy s'' arity T_args
blanchet@43179
  1264
           in
blanchet@43179
  1265
             case type_arg_policy type_sys s'' of
blanchet@43179
  1266
               Explicit_Type_Args drop_args =>
blanchet@43179
  1267
               (name, filtered_T_args drop_args)
blanchet@43179
  1268
             | Mangled_Type_Args drop_args =>
blanchet@43179
  1269
               (mangled_const_name format type_sys (filtered_T_args drop_args)
blanchet@43179
  1270
                                   name, [])
blanchet@43179
  1271
             | No_Type_Args => (name, [])
blanchet@43179
  1272
           end)
blanchet@43179
  1273
        |> (fn (name, T_args) => CombConst (name, T, T_args))
blanchet@42753
  1274
      | aux _ tm = tm
blanchet@42753
  1275
  in aux 0 end
blanchet@42573
  1276
blanchet@43179
  1277
fun repair_combterm ctxt format type_sys sym_tab =
blanchet@42994
  1278
  not (is_setting_higher_order format type_sys)
blanchet@42994
  1279
  ? (introduce_explicit_apps_in_combterm sym_tab
blanchet@42994
  1280
     #> introduce_predicators_in_combterm sym_tab)
blanchet@43179
  1281
  #> enforce_type_arg_policy_in_combterm ctxt format type_sys
blanchet@43179
  1282
fun repair_fact ctxt format type_sys sym_tab =
blanchet@42701
  1283
  update_combformula (formula_map
blanchet@43179
  1284
      (repair_combterm ctxt format type_sys sym_tab))
blanchet@42573
  1285
blanchet@42573
  1286
(** Helper facts **)
blanchet@42573
  1287
blanchet@43194
  1288
(* The Boolean indicates that a fairly sound type encoding is needed. *)
blanchet@43085
  1289
val helper_table =
blanchet@43194
  1290
  [(("COMBI", false), @{thms Meson.COMBI_def}),
blanchet@43194
  1291
   (("COMBK", false), @{thms Meson.COMBK_def}),
blanchet@43194
  1292
   (("COMBB", false), @{thms Meson.COMBB_def}),
blanchet@43194
  1293
   (("COMBC", false), @{thms Meson.COMBC_def}),
blanchet@43194
  1294
   (("COMBS", false), @{thms Meson.COMBS_def}),
blanchet@43194
  1295
   (("fequal", true),
blanchet@43085
  1296
    (* This is a lie: Higher-order equality doesn't need a sound type encoding.
blanchet@43085
  1297
       However, this is done so for backward compatibility: Including the
blanchet@43085
  1298
       equality helpers by default in Metis breaks a few existing proofs. *)
blanchet@43194
  1299
    @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
blanchet@43194
  1300
           fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
blanchet@43194
  1301
   (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
blanchet@43194
  1302
   (("fFalse", true), @{thms True_or_False}),
blanchet@43194
  1303
   (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
blanchet@43194
  1304
   (("fTrue", true), @{thms True_or_False}),
blanchet@43194
  1305
   (("fNot", false),
blanchet@43194
  1306
    @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
blanchet@43194
  1307
           fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
blanchet@43194
  1308
   (("fconj", false),
blanchet@43194
  1309
    @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
blanchet@43194
  1310
        by (unfold fconj_def) fast+}),
blanchet@43194
  1311
   (("fdisj", false),
blanchet@43194
  1312
    @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
blanchet@43194
  1313
        by (unfold fdisj_def) fast+}),
blanchet@43194
  1314
   (("fimplies", false),
blanchet@43210
  1315
    @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
blanchet@43194
  1316
        by (unfold fimplies_def) fast+}),
blanchet@43194
  1317
   (("If", true), @{thms if_True if_False True_or_False})]
blanchet@43194
  1318
  |> map (apsnd (map zero_var_indexes))
blanchet@43085
  1319
blanchet@43130
  1320
val type_tag = `make_fixed_const type_tag_name
blanchet@43130
  1321
blanchet@43159
  1322
fun type_tag_idempotence_fact () =
blanchet@42573
  1323
  let
blanchet@42573
  1324
    fun var s = ATerm (`I s, [])
blanchet@43159
  1325
    fun tag tm = ATerm (type_tag, [var "T", tm])
blanchet@43207
  1326
    val tagged_a = tag (var "A")
blanchet@42573
  1327
  in
blanchet@43159
  1328
    Formula (type_tag_idempotence_helper_name, Axiom,
blanchet@43207
  1329
             AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
blanchet@42879
  1330
             |> close_formula_universally, simp_info, NONE)
blanchet@42573
  1331
  end
blanchet@42573
  1332
blanchet@43159
  1333
fun should_specialize_helper type_sys t =
blanchet@43159
  1334
  case general_type_arg_policy type_sys of
blanchet@43159
  1335
    Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
blanchet@43159
  1336
  | _ => false
blanchet@43159
  1337
blanchet@43064
  1338
fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
blanchet@42573
  1339
  case strip_prefix_and_unascii const_prefix s of
blanchet@42573
  1340
    SOME mangled_s =>
blanchet@42573
  1341
    let
blanchet@42573
  1342
      val thy = Proof_Context.theory_of ctxt
blanchet@42573
  1343
      val unmangled_s = mangled_s |> unmangled_const_name
blanchet@43159
  1344
      fun dub_and_inst needs_fairly_sound (th, j) =
blanchet@43159
  1345
        ((unmangled_s ^ "_" ^ string_of_int j ^
blanchet@43159
  1346
          (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
blanchet@42893
  1347
          (if needs_fairly_sound then typed_helper_suffix
blanchet@42881
  1348
           else untyped_helper_suffix),
blanchet@42881
  1349
          General),
blanchet@42573
  1350
         let val t = th |> prop_of in
blanchet@43159
  1351
           t |> should_specialize_helper type_sys t
blanchet@43064
  1352
                ? (case types of
blanchet@43064
  1353
                     [T] => specialize_type thy (invert_const unmangled_s, T)
blanchet@43064
  1354
                   | _ => I)
blanchet@42573
  1355
         end)
blanchet@43159
  1356
      val make_facts =
blanchet@43264
  1357
        map_filter (make_fact ctxt format type_sys false false false [])
blanchet@42893
  1358
      val fairly_sound = is_type_sys_fairly_sound type_sys
blanchet@42573
  1359
    in
blanchet@43085
  1360
      helper_table
blanchet@43194
  1361
      |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
blanchet@43159
  1362
                  if helper_s <> unmangled_s orelse
blanchet@42894
  1363
                     (needs_fairly_sound andalso not fairly_sound) then
blanchet@42573
  1364
                    []
blanchet@42573
  1365
                  else
blanchet@42573
  1366
                    ths ~~ (1 upto length ths)
blanchet@43159
  1367
                    |> map (dub_and_inst needs_fairly_sound)
blanchet@43159
  1368
                    |> make_facts)
blanchet@42573
  1369
    end
blanchet@42573
  1370
  | NONE => []
blanchet@42962
  1371
fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
blanchet@42962
  1372
  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
blanchet@42962
  1373
                  []
blanchet@42573
  1374
blanchet@43085
  1375
(***************************************************************)
blanchet@43085
  1376
(* Type Classes Present in the Axiom or Conjecture Clauses     *)
blanchet@43085
  1377
(***************************************************************)
blanchet@43085
  1378
blanchet@43085
  1379
fun set_insert (x, s) = Symtab.update (x, ()) s
blanchet@43085
  1380
blanchet@43085
  1381
fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
blanchet@43085
  1382
blanchet@43085
  1383
(* Remove this trivial type class (FIXME: similar code elsewhere) *)
blanchet@43085
  1384
fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
blanchet@43085
  1385
blanchet@43093
  1386
fun classes_of_terms get_Ts =
blanchet@43121
  1387
  map (map snd o get_Ts)
blanchet@43093
  1388
  #> List.foldl add_classes Symtab.empty
blanchet@43093
  1389
  #> delete_type #> Symtab.keys
blanchet@43085
  1390
blanchet@43093
  1391
val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
blanchet@43093
  1392
val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
blanchet@43085
  1393
blanchet@43085
  1394
(*fold type constructors*)
blanchet@43189
  1395
fun fold_type_constrs f (Type (a, Ts)) x =
blanchet@43189
  1396
    fold (fold_type_constrs f) Ts (f (a,x))
blanchet@43189
  1397
  | fold_type_constrs _ _ x = x
blanchet@43085
  1398
blanchet@43085
  1399
(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
blanchet@43189
  1400
fun add_type_constrs_in_term thy =
blanchet@43085
  1401
  let
blanchet@43188
  1402
    fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
blanchet@43181
  1403
      | add (t $ u) = add t #> add u
blanchet@43188
  1404
      | add (Const (x as (s, _))) =
blanchet@43188
  1405
        if String.isPrefix skolem_const_prefix s then I
blanchet@43189
  1406
        else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
blanchet@43181
  1407
      | add (Abs (_, _, u)) = add u
blanchet@43181
  1408
      | add _ = I
blanchet@43181
  1409
  in add end
blanchet@43085
  1410
blanchet@43189
  1411
fun type_constrs_of_terms thy ts =
blanchet@43189
  1412
  Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
blanchet@43085
  1413
blanchet@43096
  1414
fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
blanchet@43214
  1415
                       facts =
blanchet@42573
  1416
  let
blanchet@42573
  1417
    val thy = Proof_Context.theory_of ctxt
blanchet@43222
  1418
    val fact_ts = facts |> map snd
blanchet@43264
  1419
    val presimp_consts = Meson.presimplified_consts ctxt
blanchet@43264
  1420
    val make_fact =
blanchet@43264
  1421
      make_fact ctxt format type_sys false true true presimp_consts
blanchet@42573
  1422
    val (facts, fact_names) =
blanchet@43264
  1423
      facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
blanchet@43214
  1424
            |> map_filter (try (apfst the))
blanchet@43214
  1425
            |> ListPair.unzip
blanchet@42573
  1426
    (* Remove existing facts from the conjecture, as this can dramatically
blanchet@42573
  1427
       boost an ATP's performance (for some reason). *)
blanchet@43192
  1428
    val hyp_ts =
blanchet@43192
  1429
      hyp_ts
blanchet@43192
  1430
      |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
blanchet@42573
  1431
    val goal_t = Logic.list_implies (hyp_ts, concl_t)
blanchet@42573
  1432
    val all_ts = goal_t :: fact_ts
blanchet@42573
  1433
    val subs = tfree_classes_of_terms all_ts
blanchet@42573
  1434
    val supers = tvar_classes_of_terms all_ts
blanchet@43189
  1435
    val tycons = type_constrs_of_terms thy all_ts
blanchet@42994
  1436
    val conjs =
blanchet@43096
  1437
      hyp_ts @ [concl_t]
blanchet@43264
  1438
      |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
blanchet@42573
  1439
    val (supers', arity_clauses) =
blanchet@42589
  1440
      if level_of_type_sys type_sys = No_Types then ([], [])
blanchet@42573
  1441
      else make_arity_clauses thy tycons supers
blanchet@42573
  1442
    val class_rel_clauses = make_class_rel_clauses thy subs supers'
blanchet@42573
  1443
  in
blanchet@42573
  1444
    (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
blanchet@42573
  1445
  end
blanchet@42573
  1446
blanchet@42573
  1447
fun fo_literal_from_type_literal (TyLitVar (class, name)) =
blanchet@42573
  1448
    (true, ATerm (class, [ATerm (name, [])]))
blanchet@42573
  1449
  | fo_literal_from_type_literal (TyLitFree (class, name)) =
blanchet@42573
  1450
    (true, ATerm (class, [ATerm (name, [])]))
blanchet@42573
  1451
blanchet@42573
  1452
fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
blanchet@42573
  1453
blanchet@43130
  1454
val type_pred = `make_fixed_const type_pred_name
blanchet@43130
  1455
blanchet@43179
  1456
fun type_pred_combterm ctxt format type_sys T tm =
blanchet@43179
  1457
  CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
blanchet@43179
  1458
           |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
blanchet@42573
  1459
blanchet@42878
  1460
fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
blanchet@42878
  1461
  | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
blanchet@43000
  1462
    accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
blanchet@42878
  1463
fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
blanchet@42878
  1464
  | is_var_nonmonotonic_in_formula pos phi _ name =
blanchet@42878
  1465
    formula_fold pos (var_occurs_positively_naked_in_term name) phi false
blanchet@42834
  1466
blanchet@43178
  1467
fun mk_const_aterm format type_sys x T_args args =
blanchet@43178
  1468
  ATerm (x, map (fo_term_from_typ format type_sys) T_args @ args)
blanchet@42994
  1469
blanchet@42962
  1470
fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
blanchet@43130
  1471
  CombConst (type_tag, T --> T, [T])
blanchet@43179
  1472
  |> enforce_type_arg_policy_in_combterm ctxt format type_sys
blanchet@42962
  1473
  |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
blanchet@42829
  1474
  |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
blanchet@42962
  1475
and term_from_combterm ctxt format nonmono_Ts type_sys =
blanchet@42573
  1476
  let
blanchet@42962
  1477
    fun aux site u =
blanchet@42962
  1478
      let
blanchet@42962
  1479
        val (head, args) = strip_combterm_comb u
blanchet@42962
  1480
        val (x as (s, _), T_args) =
blanchet@42962
  1481
          case head of
blanchet@42962
  1482
            CombConst (name, _, T_args) => (name, T_args)
blanchet@42962
  1483
          | CombVar (name, _) => (name, [])
blanchet@42962
  1484
          | CombApp _ => raise Fail "impossible \"CombApp\""
blanchet@43000
  1485
        val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg
blanchet@42962
  1486
                       else Elsewhere
blanchet@43178
  1487
        val t = mk_const_aterm format type_sys x T_args
blanchet@43178
  1488
                    (map (aux arg_site) args)
blanchet@42962
  1489
        val T = combtyp_of u
blanchet@42962
  1490
      in
blanchet@42962
  1491
        t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
blanchet@42962
  1492
                tag_with_type ctxt format nonmono_Ts type_sys T
blanchet@42962
  1493
              else
blanchet@42962
  1494
                I)
blanchet@42962
  1495
      end
blanchet@42962
  1496
  in aux end
blanchet@42962
  1497
and formula_from_combformula ctxt format nonmono_Ts type_sys
blanchet@42962
  1498
                             should_predicate_on_var =
blanchet@42829
  1499
  let
blanchet@42962
  1500
    val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
blanchet@42573
  1501
    val do_bound_type =
blanchet@42682
  1502
      case type_sys of
blanchet@42722
  1503
        Simple_Types level =>
blanchet@42994
  1504
        homogenized_type ctxt nonmono_Ts level 0
blanchet@43178
  1505
        #> mangled_type format type_sys false 0 #> SOME
blanchet@42682
  1506
      | _ => K NONE
blanchet@42878
  1507
    fun do_out_of_bound_type pos phi universal (name, T) =
blanchet@42834
  1508
      if should_predicate_on_type ctxt nonmono_Ts type_sys
blanchet@42878
  1509
             (fn () => should_predicate_on_var pos phi universal name) T then
blanchet@42834
  1510
        CombVar (name, T)
blanchet@43179
  1511
        |> type_pred_combterm ctxt format type_sys T
blanchet@42878
  1512
        |> do_term |> AAtom |> SOME
blanchet@42573
  1513
      else
blanchet@42573
  1514
        NONE
blanchet@42878
  1515
    fun do_formula pos (AQuant (q, xs, phi)) =
blanchet@42878
  1516
        let
blanchet@42878
  1517
          val phi = phi |> do_formula pos
blanchet@42878
  1518
          val universal = Option.map (q = AExists ? not) pos
blanchet@42878
  1519
        in
blanchet@42834
  1520
          AQuant (q, xs |> map (apsnd (fn NONE => NONE
blanchet@42834
  1521
                                        | SOME T => do_bound_type T)),
blanchet@42834
  1522
                  (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
blanchet@42834
  1523
                      (map_filter
blanchet@42834
  1524
                           (fn (_, NONE) => NONE
blanchet@42834
  1525
                             | (s, SOME T) =>
blanchet@42878
  1526
                               do_out_of_bound_type pos phi universal (s, T))
blanchet@42878
  1527
                           xs)
blanchet@42834
  1528
                      phi)
blanchet@42834
  1529
        end
blanchet@42878
  1530
      | do_formula pos (AConn conn) = aconn_map pos do_formula conn
blanchet@42878
  1531
      | do_formula _ (AAtom tm) = AAtom (do_term tm)
blanchet@42878
  1532
  in do_formula o SOME end
blanchet@42573
  1533
blanchet@43098
  1534
fun bound_tvars type_sys Ts =
blanchet@42727
  1535
  mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
blanchet@43263
  1536
                (type_literals_for_types type_sys add_sorts_on_tvar Ts))
blanchet@42727
  1537
blanchet@42956
  1538
fun formula_for_fact ctxt format nonmono_Ts type_sys
blanchet@42573
  1539
                     ({combformula, atomic_types, ...} : translated_formula) =
blanchet@42727
  1540
  combformula
blanchet@42727
  1541
  |> close_combformula_universally
blanchet@42962
  1542
  |> formula_from_combformula ctxt format nonmono_Ts type_sys
blanchet@42878
  1543
                              is_var_nonmonotonic_in_formula true
blanchet@43098
  1544
  |> bound_tvars type_sys atomic_types
blanchet@42573
  1545
  |> close_formula_universally
blanchet@42573
  1546
blanchet@42573
  1547
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
blanchet@42573
  1548
   of monomorphization). The TPTP explicitly forbids name clashes, and some of
blanchet@42573
  1549
   the remote provers might care. *)
blanchet@43159
  1550
fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
blanchet@42640
  1551
                          (j, formula as {name, locality, kind, ...}) =
blanchet@43159
  1552
  Formula (prefix ^
blanchet@43159
  1553
           (if freshen andalso
blanchet@43159
  1554
               polymorphism_of_type_sys type_sys <> Polymorphic then
blanchet@43159
  1555
              string_of_int j ^ "_"
blanchet@43159
  1556
            else
blanchet@43159
  1557
              "") ^ encode name,
blanchet@42956
  1558
           kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
blanchet@42879
  1559
           case locality of
blanchet@42879
  1560
             Intro => intro_info
blanchet@42879
  1561
           | Elim => elim_info
blanchet@42879
  1562
           | Simp => simp_info
blanchet@42879
  1563
           | _ => NONE)
blanchet@42573
  1564
blanchet@43086
  1565
fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
blanchet@43086
  1566
                                       : class_rel_clause) =
blanchet@42573
  1567
  let val ty_arg = ATerm (`I "T", []) in
blanchet@42577
  1568
    Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
blanchet@42573
  1569
             AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
blanchet@42573
  1570
                               AAtom (ATerm (superclass, [ty_arg]))])
blanchet@42879
  1571
             |> close_formula_universally, intro_info, NONE)
blanchet@42573
  1572
  end
blanchet@42573
  1573
blanchet@42573
  1574
fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
blanchet@42573
  1575
    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
blanchet@42573
  1576
  | fo_literal_from_arity_literal (TVarLit (c, sort)) =
blanchet@42573
  1577
    (false, ATerm (c, [ATerm (sort, [])]))
blanchet@42573
  1578
blanchet@43086
  1579
fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
blanchet@43086
  1580
                                   : arity_clause) =
blanchet@42577
  1581
  Formula (arity_clause_prefix ^ ascii_of name, Axiom,
blanchet@42573
  1582
           mk_ahorn (map (formula_from_fo_literal o apfst not
blanchet@42895
  1583
                          o fo_literal_from_arity_literal) prem_lits)
blanchet@42573
  1584
                    (formula_from_fo_literal
blanchet@42895
  1585
                         (fo_literal_from_arity_literal concl_lits))
blanchet@42879
  1586
           |> close_formula_universally, intro_info, NONE)
blanchet@42573
  1587
blanchet@42962
  1588
fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
blanchet@43098
  1589
        ({name, kind, combformula, atomic_types, ...} : translated_formula) =
blanchet@42577
  1590
  Formula (conjecture_prefix ^ name, kind,
blanchet@42962
  1591
           formula_from_combformula ctxt format nonmono_Ts type_sys
blanchet@42939
  1592
               is_var_nonmonotonic_in_formula false
blanchet@42939
  1593
               (close_combformula_universally combformula)
blanchet@43098
  1594
           |> bound_tvars type_sys atomic_types
blanchet@42573
  1595
           |> close_formula_universally, NONE, NONE)
blanchet@42573
  1596
blanchet@43098
  1597
fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
blanchet@43263
  1598
  atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
blanchet@42573
  1599
               |> map fo_literal_from_type_literal
blanchet@42573
  1600
blanchet@42573
  1601
fun formula_line_for_free_type j lit =
blanchet@43085
  1602
  Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
blanchet@42573
  1603
           formula_from_fo_literal lit, NONE, NONE)
blanchet@43098
  1604
fun formula_lines_for_free_types type_sys facts =
blanchet@42573
  1605
  let
blanchet@43098
  1606
    val litss = map (free_type_literals type_sys) facts
blanchet@42573
  1607
    val lits = fold (union (op =)) litss []
blanchet@42573
  1608
  in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
blanchet@42573
  1609
blanchet@42573
  1610
(** Symbol declarations **)
blanchet@42544
  1611
blanchet@42574
  1612
fun should_declare_sym type_sys pred_sym s =
blanchet@42998
  1613
  is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
blanchet@42894
  1614
  (case type_sys of
blanchet@42894
  1615
     Simple_Types _ => true
blanchet@43128
  1616
   | Tags (_, _, Lightweight) => true
blanchet@42894
  1617
   | _ => not pred_sym)
blanchet@38282
  1618
blanchet@42886
  1619
fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
blanchet@42574
  1620
  let
blanchet@42698
  1621
    fun add_combterm in_conj tm =
blanchet@42574
  1622
      let val (head, args) = strip_combterm_comb tm in
blanchet@42574
  1623
        (case head of
blanchet@42574
  1624
           CombConst ((s, s'), T, T_args) =>
blanchet@42574
  1625
           let val pred_sym = is_pred_sym repaired_sym_tab s in
blanchet@42574
  1626
             if should_declare_sym type_sys pred_sym s then
blanchet@42576
  1627
               Symtab.map_default (s, [])
blanchet@42886
  1628
                   (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
blanchet@42886
  1629
                                         in_conj))
blanchet@42574
  1630
             else
blanchet@42574
  1631
               I
blanchet@42574
  1632
           end
blanchet@42574
  1633
         | _ => I)
blanchet@42698
  1634
        #> fold (add_combterm in_conj) args
blanchet@42574
  1635
      end
blanchet@42698
  1636
    fun add_fact in_conj =
blanchet@42834
  1637
      fact_lift (formula_fold NONE (K (add_combterm in_conj)))
blanchet@42698
  1638
  in
blanchet@42698
  1639
    Symtab.empty
blanchet@42698
  1640
    |> is_type_sys_fairly_sound type_sys
blanchet@42698
  1641
       ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
blanchet@42698
  1642
  end
blanchet@42533
  1643
blanchet@42886
  1644
(* These types witness that the type classes they belong to allow infinite
blanchet@42886
  1645
   models and hence that any types with these type classes is monotonic. *)
blanchet@43085
  1646
val known_infinite_types =
blanchet@43085
  1647
  [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
blanchet@42886
  1648
blanchet@42685
  1649
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
blanchet@42685
  1650
   out with monotonicity" paper presented at CADE 2011. *)
blanchet@43293
  1651
fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
blanchet@43293
  1652
  | add_combterm_nonmonotonic_types ctxt level locality _
blanchet@43179
  1653
        (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
blanchet@43179
  1654
                           tm2)) =
blanchet@43000
  1655
    (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
blanchet@42829
  1656
     (case level of
blanchet@42886
  1657
        Nonmonotonic_Types =>
blanchet@43293
  1658
        not (is_locality_global locality) orelse
blanchet@42886
  1659
        not (is_type_surely_infinite ctxt known_infinite_types T)
blanchet@42829
  1660
      | Finite_Types => is_type_surely_finite ctxt T
blanchet@42886
  1661
      | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
blanchet@43293
  1662
  | add_combterm_nonmonotonic_types _ _ _ _ _ = I
blanchet@43293
  1663
fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...}
blanchet@42829
  1664
                                            : translated_formula) =
blanchet@42834
  1665
  formula_fold (SOME (kind <> Conjecture))
blanchet@43293
  1666
               (add_combterm_nonmonotonic_types ctxt level locality) combformula
blanchet@42886
  1667
fun nonmonotonic_types_for_facts ctxt type_sys facts =
blanchet@42829
  1668
  let val level = level_of_type_sys type_sys in
blanchet@42886
  1669
    if level = Nonmonotonic_Types orelse level = Finite_Types then
blanchet@42886
  1670
      [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
blanchet@42886
  1671
         (* We must add "bool" in case the helper "True_or_False" is added
blanchet@42886
  1672
            later. In addition, several places in the code rely on the list of
blanchet@42886
  1673
            nonmonotonic types not being empty. *)
blanchet@42886
  1674
         |> insert_type ctxt I @{typ bool}
blanchet@42886
  1675
    else
blanchet@42886
  1676
      []
blanchet@42829
  1677
  end
blanchet@42677
  1678
blanchet@42994
  1679
fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
blanchet@42994
  1680
                      (s', T_args, T, pred_sym, ary, _) =
blanchet@42994
  1681
  let
blanchet@43178
  1682
    val (T_arg_Ts, level) =
blanchet@42994
  1683
      case type_sys of
blanchet@43178
  1684
        Simple_Types level => ([], level)
blanchet@43178
  1685
      | _ => (replicate (length T_args) homo_infinite_type, No_Types)
blanchet@42994
  1686
  in
blanchet@42998
  1687
    Decl (sym_decl_prefix ^ s, (s, s'),
blanchet@42994
  1688
          (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
blanchet@43178
  1689
          |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
blanchet@42994
  1690
  end
blanchet@42579
  1691
blanchet@42592
  1692
fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
blanchet@42592
  1693
blanchet@43125
  1694
fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
blanchet@43125
  1695
        type_sys n s j (s', T_args, T, _, ary, in_conj) =
blanchet@42579
  1696
  let
blanchet@42709
  1697
    val (kind, maybe_negate) =
blanchet@42709
  1698
      if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
blanchet@42709
  1699
      else (Axiom, I)
blanchet@42753
  1700
    val (arg_Ts, res_T) = chop_fun ary T
blanchet@42579
  1701
    val bound_names =
blanchet@42579
  1702
      1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
blanchet@42829
  1703
    val bounds =
blanchet@42579
  1704
      bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
blanchet@42579
  1705
    val bound_Ts =
blanchet@42592
  1706
      arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
blanchet@42592
  1707
                             else NONE)
blanchet@42579
  1708
  in
blanchet@43125
  1709
    Formula (preds_sym_formula_prefix ^ s ^
blanchet@42709
  1710
             (if n > 1 then "_" ^ string_of_int j else ""), kind,
blanchet@42579
  1711
             CombConst ((s, s'), T, T_args)
blanchet@42829
  1712
             |> fold (curry (CombApp o swap)) bounds
blanchet@43179
  1713
             |> type_pred_combterm ctxt format type_sys res_T
blanchet@42963
  1714
             |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
blanchet@42962
  1715
             |> formula_from_combformula ctxt format nonmono_Ts type_sys
blanchet@42878
  1716
                                         (K (K (K (K true)))) true
blanchet@43098
  1717
             |> n > 1 ? bound_tvars type_sys (atyps_of T)
blanchet@42709
  1718
             |> close_formula_universally
blanchet@42709
  1719
             |> maybe_negate,
blanchet@42879
  1720
             intro_info, NONE)
blanchet@42579
  1721
  end
blanchet@42579
  1722
blanchet@43129
  1723
fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
blanchet@43129
  1724
        nonmono_Ts type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
blanchet@42829
  1725
  let
blanchet@42829
  1726
    val ident_base =
blanchet@43129
  1727
      lightweight_tags_sym_formula_prefix ^ s ^
blanchet@43125
  1728
      (if n > 1 then "_" ^ string_of_int j else "")
blanchet@42852
  1729
    val (kind, maybe_negate) =
blanchet@42852
  1730
      if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
blanchet@42852
  1731
      else (Axiom, I)
blanchet@42829
  1732
    val (arg_Ts, res_T) = chop_fun ary T
blanchet@42829
  1733
    val bound_names =
blanchet@42829
  1734
      1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
blanchet@42829
  1735
    val bounds = bound_names |> map (fn name => ATerm (name, []))
blanchet@43178
  1736
    val cst = mk_const_aterm format type_sys (s, s') T_args
blanchet@42830
  1737
    val atomic_Ts = atyps_of T
blanchet@42834
  1738
    fun eq tms =
blanchet@42834
  1739
      (if pred_sym then AConn (AIff, map AAtom tms)
blanchet@43000
  1740
       else AAtom (ATerm (`I tptp_equal, tms)))
blanchet@43098
  1741
      |> bound_tvars type_sys atomic_Ts
blanchet@42830
  1742
      |> close_formula_universally
blanchet@42852
  1743
      |> maybe_negate
blanchet@42836
  1744
    val should_encode = should_encode_type ctxt nonmono_Ts All_Types
blanchet@42962
  1745
    val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
blanchet@42829
  1746
    val add_formula_for_res =
blanchet@42829
  1747
      if should_encode res_T then
blanchet@42852
  1748
        cons (Formula (ident_base ^ "_res", kind,
blanchet@42994
  1749
                       eq [tag_with res_T (cst bounds), cst bounds],
blanchet@42879
  1750
                       simp_info, NONE))
blanchet@42829
  1751
      else
blanchet@42829
  1752
        I
blanchet@42829
  1753
    fun add_formula_for_arg k =
blanchet@42829
  1754
      let val arg_T = nth arg_Ts k in
blanchet@42829
  1755
        if should_encode arg_T then
blanchet@42829
  1756
          case chop k bounds of
blanchet@42829
  1757
            (bounds1, bound :: bounds2) =>
blanchet@42852
  1758
            cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
blanchet@42994
  1759
                           eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
blanchet@42994
  1760
                               cst bounds],
blanchet@42879
  1761
                           simp_info, NONE))
blanchet@42829
  1762
          | _ => raise Fail "expected nonempty tail"
blanchet@42829
  1763
        else
blanchet@42829
  1764
          I
blanchet@42829
  1765
      end
blanchet@42829
  1766
  in
blanchet@42834
  1767
    [] |> not pred_sym ? add_formula_for_res
blanchet@42829
  1768
       |> fold add_formula_for_arg (ary - 1 downto 0)
blanchet@42829
  1769
  end
blanchet@42829
  1770
blanchet@42836
  1771
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
blanchet@42836
  1772
blanchet@42956
  1773
fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
blanchet@42709
  1774
                                (s, decls) =
blanchet@42998
  1775
  case type_sys of
blanchet@42998
  1776
    Simple_Types _ =>
blanchet@42998
  1777
    decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
blanchet@42998
  1778
  | Preds _ =>
blanchet@42998
  1779
    let
blanchet@42998
  1780
      val decls =
blanchet@42998
  1781
        case decls of
blanchet@42998
  1782
          decl :: (decls' as _ :: _) =>
blanchet@42998
  1783
          let val T = result_type_of_decl decl in
blanchet@42998
  1784
            if forall (curry (type_instance ctxt o swap) T
blanchet@42998
  1785
                       o result_type_of_decl) decls' then
blanchet@42998
  1786
              [decl]
blanchet@42998
  1787
            else
blanchet@42998
  1788
              decls
blanchet@42998
  1789
          end
blanchet@42998
  1790
        | _ => decls
blanchet@42998
  1791
      val n = length decls
blanchet@42998
  1792
      val decls =
blanchet@42998
  1793
        decls
blanchet@42998
  1794
        |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
blanchet@42998
  1795
                   o result_type_of_decl)
blanchet@42998
  1796
    in
blanchet@42998
  1797
      (0 upto length decls - 1, decls)
blanchet@43125
  1798
      |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
blanchet@43125
  1799
                                                nonmono_Ts type_sys n s)
blanchet@42998
  1800
    end
blanchet@42998
  1801
  | Tags (_, _, heaviness) =>
blanchet@42998
  1802
    (case heaviness of
blanchet@43128
  1803
       Heavyweight => []
blanchet@43128
  1804
     | Lightweight =>
blanchet@42998
  1805
       let val n = length decls in
blanchet@42998
  1806
         (0 upto n - 1 ~~ decls)
blanchet@43129
  1807
         |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
blanchet@43129
  1808
                      conj_sym_kind nonmono_Ts type_sys n s)
blanchet@42998
  1809
       end)
blanchet@42579
  1810
blanchet@42956
  1811
fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
blanchet@42956
  1812
                                     type_sys sym_decl_tab =
blanchet@42998
  1813
  sym_decl_tab
blanchet@42998
  1814
  |> Symtab.dest
blanchet@42998
  1815
  |> sort_wrt fst
blanchet@42998
  1816
  |> rpair []
blanchet@42998
  1817
  |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
blanchet@42998
  1818
                                                     nonmono_Ts type_sys)
blanchet@42543
  1819
blanchet@43185
  1820
fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
blanchet@43185
  1821
    poly <> Mangled_Monomorphic andalso
blanchet@43185
  1822
    ((level = All_Types andalso heaviness = Lightweight) orelse
blanchet@43185
  1823
     level = Nonmonotonic_Types orelse level = Finite_Types)
blanchet@43159
  1824
  | needs_type_tag_idempotence _ = false
blanchet@42831
  1825
blanchet@42939
  1826
fun offset_of_heading_in_problem _ [] j = j
blanchet@42939
  1827
  | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
blanchet@42939
  1828
    if heading = needle then j
blanchet@42939
  1829
    else offset_of_heading_in_problem needle problem (j + length lines)
blanchet@42939
  1830
blanchet@42998
  1831
val implicit_declsN = "Should-be-implicit typings"
blanchet@42998
  1832
val explicit_declsN = "Explicit typings"
blanchet@41157
  1833
val factsN = "Relevant facts"
blanchet@41157
  1834
val class_relsN = "Class relationships"
blanchet@42543
  1835
val aritiesN = "Arities"
blanchet@41157
  1836
val helpersN = "Helper facts"
blanchet@41157
  1837
val conjsN = "Conjectures"
blanchet@41313
  1838
val free_typesN = "Type variables"
blanchet@41157
  1839
blanchet@43259
  1840
val explicit_apply = NONE (* for experimental purposes *)
blanchet@43259
  1841
blanchet@42939
  1842
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
blanchet@43259
  1843
                        readable_names preproc hyp_ts concl_t facts =
blanchet@38282
  1844
  let
blanchet@43101
  1845
    val (format, type_sys) = choose_format [format] type_sys
blanchet@41313
  1846
    val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
blanchet@43096
  1847
      translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
blanchet@43096
  1848
                         facts
blanchet@43064
  1849
    val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
blanchet@42886
  1850
    val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
blanchet@43179
  1851
    val repair = repair_fact ctxt format type_sys sym_tab
blanchet@42682
  1852
    val (conjs, facts) = (conjs, facts) |> pairself (map repair)
blanchet@43064
  1853
    val repaired_sym_tab =
blanchet@43064
  1854
      conjs @ facts |> sym_table_for_facts ctxt (SOME false)
blanchet@42573
  1855
    val helpers =
blanchet@42962
  1856
      repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
blanchet@42962
  1857
                       |> map repair
blanchet@42894
  1858
    val lavish_nonmono_Ts =
blanchet@43213
  1859
      if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
blanchet@42894
  1860
         polymorphism_of_type_sys type_sys <> Polymorphic then
blanchet@42894
  1861
        nonmono_Ts
blanchet@42894
  1862
      else
blanchet@42894
  1863
        [TVar (("'a", 0), HOLogic.typeS)]
blanchet@42680
  1864
    val sym_decl_lines =
blanchet@42731
  1865
      (conjs, helpers @ facts)
blanchet@42886
  1866
      |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
blanchet@42956
  1867
      |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind
blanchet@42956
  1868
                                          lavish_nonmono_Ts type_sys
blanchet@42881
  1869
    val helper_lines =
blanchet@42956
  1870
      0 upto length helpers - 1 ~~ helpers
blanchet@43159
  1871
      |> map (formula_line_for_fact ctxt format helper_prefix I false
blanchet@43159
  1872
                                    lavish_nonmono_Ts type_sys)
blanchet@43159
  1873
      |> (if needs_type_tag_idempotence type_sys then
blanchet@43159
  1874
            cons (type_tag_idempotence_fact ())
blanchet@43159
  1875
          else
blanchet@43159
  1876
            I)
blanchet@42522
  1877
    (* Reordering these might confuse the proof reconstruction code or the SPASS
blanchet@43039
  1878
       FLOTTER hack. *)
blanchet@38282
  1879
    val problem =
blanchet@42998
  1880
      [(explicit_declsN, sym_decl_lines),
blanchet@42956
  1881
       (factsN,
blanchet@43159
  1882
        map (formula_line_for_fact ctxt format fact_prefix ascii_of true
blanchet@43159
  1883
                                   nonmono_Ts type_sys)
blanchet@42956
  1884
            (0 upto length facts - 1 ~~ facts)),
blanchet@42545
  1885
       (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
blanchet@42545
  1886
       (aritiesN, map formula_line_for_arity_clause arity_clauses),
blanchet@42881
  1887
       (helpersN, helper_lines),
blanchet@42962
  1888
       (conjsN,
blanchet@42962
  1889
        map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
blanchet@42962
  1890
            conjs),
blanchet@43098
  1891
       (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
blanchet@42543
  1892
    val problem =
blanchet@42561
  1893
      problem
blanchet@43092
  1894
      |> (case format of
blanchet@43092
  1895
            CNF => ensure_cnf_problem
blanchet@43092
  1896
          | CNF_UEQ => filter_cnf_ueq_problem
blanchet@43092
  1897
          | _ => I)
blanchet@42998
  1898
      |> (if is_format_typed format then
blanchet@42998
  1899
            declare_undeclared_syms_in_atp_problem type_decl_prefix
blanchet@42998
  1900
                                                   implicit_declsN
blanchet@42998
  1901
          else
blanchet@42998
  1902
            I)
blanchet@43092
  1903
    val (problem, pool) = problem |> nice_atp_problem readable_names
blanchet@42881
  1904
    val helpers_offset = offset_of_heading_in_problem helpersN problem 0
blanchet@42881
  1905
    val typed_helpers =
blanchet@42881
  1906
      map_filter (fn (j, {name, ...}) =>
blanchet@42881
  1907
                     if String.isSuffix typed_helper_suffix name then SOME j
blanchet@42881
  1908
                     else NONE)
blanchet@42881
  1909
                 ((helpers_offset + 1 upto helpers_offset + length helpers)
blanchet@42881
  1910
                  ~~ helpers)
blanchet@42778
  1911
    fun add_sym_arity (s, {min_ary, ...} : sym_info) =
blanchet@42755
  1912
      if min_ary > 0 then
blanchet@42755
  1913
        case strip_prefix_and_unascii const_prefix s of
blanchet@42755
  1914
          SOME s => Symtab.insert (op =) (s, min_ary)
blanchet@42755
  1915
        | NONE => I
blanchet@42755
  1916
      else
blanchet@42755
  1917
        I
blanchet@38282
  1918
  in
blanchet@38282
  1919
    (problem,
blanchet@38282
  1920
     case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
blanchet@42585
  1921
     offset_of_heading_in_problem conjsN problem 0,
blanchet@42541
  1922
     offset_of_heading_in_problem factsN problem 0,
blanchet@42755
  1923
     fact_names |> Vector.fromList,
blanchet@42881
  1924
     typed_helpers,
blanchet@42755
  1925
     Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
blanchet@38282
  1926
  end
blanchet@38282
  1927
blanchet@41313
  1928
(* FUDGE *)
blanchet@41313
  1929
val conj_weight = 0.0
blanchet@41770
  1930
val hyp_weight = 0.1
blanchet@41770
  1931
val fact_min_weight = 0.2
blanchet@41313
  1932
val fact_max_weight = 1.0
blanchet@42608
  1933
val type_info_default_weight = 0.8
blanchet@41313
  1934
blanchet@41313
  1935
fun add_term_weights weight (ATerm (s, tms)) =
blanchet@42998
  1936
  is_tptp_user_symbol s ? Symtab.default (s, weight)
blanchet@41313
  1937
  #> fold (add_term_weights weight) tms
blanchet@42577
  1938
fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
blanchet@42834
  1939
    formula_fold NONE (K (add_term_weights weight)) phi
blanchet@42528
  1940
  | add_problem_line_weights _ _ = I
blanchet@41313
  1941
blanchet@41313
  1942
fun add_conjectures_weights [] = I
blanchet@41313
  1943
  | add_conjectures_weights conjs =
blanchet@41313
  1944
    let val (hyps, conj) = split_last conjs in
blanchet@41313
  1945
      add_problem_line_weights conj_weight conj
blanchet@41313
  1946
      #> fold (add_problem_line_weights hyp_weight) hyps
blanchet@41313
  1947
    end
blanchet@41313
  1948
blanchet@41313
  1949
fun add_facts_weights facts =
blanchet@41313
  1950
  let
blanchet@41313
  1951
    val num_facts = length facts
blanchet@41313
  1952
    fun weight_of j =
blanchet@41313
  1953
      fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
blanchet@41313
  1954
                        / Real.fromInt num_facts
blanchet@41313
  1955
  in
blanchet@41313
  1956
    map weight_of (0 upto num_facts - 1) ~~ facts
blanchet@41313
  1957
    |> fold (uncurry add_problem_line_weights)
blanchet@41313
  1958
  end
blanchet@41313
  1959
blanchet@41313
  1960
(* Weights are from 0.0 (most important) to 1.0 (least important). *)
blanchet@41313
  1961
fun atp_problem_weights problem =
blanchet@42608
  1962
  let val get = these o AList.lookup (op =) problem in
blanchet@42608
  1963
    Symtab.empty
blanchet@42608
  1964
    |> add_conjectures_weights (get free_typesN @ get conjsN)
blanchet@42608
  1965
    |> add_facts_weights (get factsN)
blanchet@42608
  1966
    |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
blanchet@42998
  1967
            [explicit_declsN, class_relsN, aritiesN]
blanchet@42608
  1968
    |> Symtab.dest
blanchet@42608
  1969
    |> sort (prod_ord Real.compare string_ord o pairself swap)
blanchet@42608
  1970
  end
blanchet@41313
  1971
blanchet@38282
  1972
end;