src/HOL/Tools/ATP/atp_problem_generate.ML
author wenzelm
Sat Mar 22 18:19:57 2014 +0100 (2014-03-22)
changeset 56254 a2dd9200854d
parent 56245 84fc7dfa3cd4
child 56636 bb8b37480d3f
permissions -rw-r--r--
more antiquotations;
blanchet@46320
     1
(*  Title:      HOL/Tools/ATP/atp_problem_generate.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@43863
     6
Translation of HOL to FOL for Metis and Sledgehammer.
blanchet@38282
     7
*)
blanchet@38282
     8
blanchet@46320
     9
signature ATP_PROBLEM_GENERATE =
blanchet@38282
    10
sig
blanchet@53586
    11
  type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
blanchet@53586
    12
  type atp_connective = ATP_Problem.atp_connective
blanchet@53586
    13
  type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
blanchet@45301
    14
  type atp_format = ATP_Problem.atp_format
blanchet@53586
    15
  type atp_formula_role = ATP_Problem.atp_formula_role
blanchet@53586
    16
  type 'a atp_problem = 'a ATP_Problem.atp_problem
blanchet@43085
    17
blanchet@54434
    18
  datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator
blanchet@47946
    19
blanchet@46340
    20
  datatype scope = Global | Local | Assum | Chained
blanchet@55212
    21
  datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
blanchet@55212
    22
blanchet@46340
    23
  type stature = scope * status
blanchet@42613
    24
blanchet@46301
    25
  datatype strictness = Strict | Non_Strict
blanchet@48183
    26
  datatype uniformity = Uniform | Non_Uniform
blanchet@52026
    27
  datatype ctr_optim = With_Ctr_Optim | Without_Ctr_Optim
blanchet@42613
    28
  datatype type_level =
blanchet@44397
    29
    All_Types |
blanchet@48200
    30
    Undercover_Types |
blanchet@48183
    31
    Nonmono_Types of strictness * uniformity |
blanchet@52026
    32
    Const_Types of ctr_optim |
blanchet@43362
    33
    No_Types
blanchet@44782
    34
  type type_enc
blanchet@42613
    35
blanchet@45513
    36
  val no_lamsN : string
blanchet@45513
    37
  val hide_lamsN : string
blanchet@46365
    38
  val liftingN : string
blanchet@46365
    39
  val combsN : string
blanchet@46365
    40
  val combs_and_liftingN : string
blanchet@46365
    41
  val combs_or_liftingN : string
blanchet@45513
    42
  val lam_liftingN : string
blanchet@45513
    43
  val keep_lamsN : string
blanchet@43496
    44
  val schematic_var_prefix : string
blanchet@43496
    45
  val fixed_var_prefix : string
blanchet@43496
    46
  val tvar_prefix : string
blanchet@43496
    47
  val tfree_prefix : string
blanchet@43496
    48
  val const_prefix : string
blanchet@43496
    49
  val type_const_prefix : string
blanchet@43496
    50
  val class_prefix : string
blanchet@45554
    51
  val lam_lifted_prefix : string
blanchet@45554
    52
  val lam_lifted_mono_prefix : string
blanchet@45554
    53
  val lam_lifted_poly_prefix : string
blanchet@43085
    54
  val skolem_const_prefix : string
blanchet@43085
    55
  val old_skolem_const_prefix : string
blanchet@43085
    56
  val new_skolem_const_prefix : string
blanchet@45554
    57
  val combinator_prefix : string
blanchet@48142
    58
  val class_decl_prefix : string
blanchet@43125
    59
  val type_decl_prefix : string
blanchet@43125
    60
  val sym_decl_prefix : string
blanchet@52004
    61
  val datatype_decl_prefix : string
blanchet@48142
    62
  val class_memb_prefix : string
blanchet@43989
    63
  val guards_sym_formula_prefix : string
blanchet@44396
    64
  val tags_sym_formula_prefix : string
blanchet@40204
    65
  val fact_prefix : string
blanchet@38282
    66
  val conjecture_prefix : string
blanchet@42881
    67
  val helper_prefix : string
blanchet@48142
    68
  val subclass_prefix : string
blanchet@48142
    69
  val tcon_clause_prefix : string
blanchet@43125
    70
  val tfree_clause_prefix : string
blanchet@45554
    71
  val lam_fact_prefix : string
blanchet@42881
    72
  val typed_helper_suffix : string
blanchet@43125
    73
  val untyped_helper_suffix : string
blanchet@42966
    74
  val predicator_name : string
blanchet@42966
    75
  val app_op_name : string
blanchet@44396
    76
  val type_guard_name : string
blanchet@43104
    77
  val type_tag_name : string
blanchet@46435
    78
  val native_type_prefix : string
blanchet@43174
    79
  val prefixed_predicator_name : string
blanchet@43130
    80
  val prefixed_app_op_name : string
blanchet@43130
    81
  val prefixed_type_tag_name : string
blanchet@43496
    82
  val ascii_of : string -> string
blanchet@43496
    83
  val unascii_of : string -> string
blanchet@45511
    84
  val unprefix_and_unascii : string -> string -> string option
blanchet@43159
    85
  val proxy_table : (string * (string * (thm * (string * string)))) list
blanchet@43159
    86
  val proxify_const : string -> (string * string) option
blanchet@43496
    87
  val invert_const : string -> string
blanchet@43496
    88
  val unproxify_const : string -> string
blanchet@52031
    89
  val new_skolem_var_name_of_const : string -> string
blanchet@48318
    90
  val atp_logical_consts : string list
blanchet@43248
    91
  val atp_irrelevant_consts : string list
blanchet@48324
    92
  val atp_widely_irrelevant_consts : string list
blanchet@54089
    93
  val is_irrelevant_const : string -> bool
blanchet@54089
    94
  val is_widely_irrelevant_const : string -> bool
blanchet@43248
    95
  val atp_schematic_consts_of : term -> typ list Symtab.table
blanchet@43828
    96
  val is_type_enc_higher_order : type_enc -> bool
blanchet@48131
    97
  val is_type_enc_polymorphic : type_enc -> bool
blanchet@43626
    98
  val level_of_type_enc : type_enc -> type_level
blanchet@48089
    99
  val is_type_enc_sound : type_enc -> bool
blanchet@52031
   100
  val type_enc_of_string : strictness -> string -> type_enc
blanchet@45301
   101
  val adjust_type_enc : atp_format -> type_enc -> type_enc
blanchet@48302
   102
  val is_lambda_free : term -> bool
blanchet@43136
   103
  val mk_aconns :
blanchet@53586
   104
    atp_connective -> ('a, 'b, 'c, 'd) atp_formula list
blanchet@53586
   105
    -> ('a, 'b, 'c, 'd) atp_formula
blanchet@53586
   106
  val unmangled_const : string -> string * (string, 'b) atp_term list
blanchet@46392
   107
  val unmangled_const_name : string -> string list
blanchet@47946
   108
  val helper_table : ((string * bool) * (status * thm) list) list
blanchet@52031
   109
  val trans_lams_of_string :
blanchet@45514
   110
    Proof.context -> type_enc -> string -> term list -> term list * term list
blanchet@48438
   111
  val string_of_status : status -> string
blanchet@43501
   112
  val factsN : string
blanchet@40059
   113
  val prepare_atp_problem :
blanchet@53586
   114
    Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode
blanchet@53586
   115
    -> string -> bool -> bool -> bool -> term list -> term
blanchet@46340
   116
    -> ((string * stature) * term) list
blanchet@53586
   117
    -> string atp_problem * string Symtab.table * (string * stature) list vector
blanchet@45551
   118
       * (string * term) list * int Symtab.table
blanchet@53586
   119
  val atp_problem_selection_weights : string atp_problem -> (string * real) list
blanchet@53586
   120
  val atp_problem_term_order_info : string atp_problem -> (string * int) list
blanchet@38282
   121
end;
blanchet@38282
   122
blanchet@46320
   123
structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
blanchet@38282
   124
struct
blanchet@38282
   125
blanchet@43085
   126
open ATP_Util
blanchet@38282
   127
open ATP_Problem
blanchet@43085
   128
blanchet@54434
   129
datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator
blanchet@47946
   130
blanchet@47768
   131
datatype scope = Global | Local | Assum | Chained
blanchet@55212
   132
datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
blanchet@55212
   133
blanchet@47768
   134
type stature = scope * status
blanchet@47768
   135
blanchet@47768
   136
datatype order =
blanchet@47768
   137
  First_Order |
blanchet@48004
   138
  Higher_Order of thf_choice
blanchet@48131
   139
datatype phantom_policy = Without_Phantom_Type_Vars | With_Phantom_Type_Vars
blanchet@48131
   140
datatype polymorphism =
blanchet@48131
   141
  Type_Class_Polymorphic |
blanchet@48131
   142
  Raw_Polymorphic of phantom_policy |
blanchet@48131
   143
  Raw_Monomorphic |
blanchet@48131
   144
  Mangled_Monomorphic
blanchet@47768
   145
datatype strictness = Strict | Non_Strict
blanchet@48183
   146
datatype uniformity = Uniform | Non_Uniform
blanchet@52026
   147
datatype ctr_optim = With_Ctr_Optim | Without_Ctr_Optim
blanchet@47768
   148
datatype type_level =
blanchet@47768
   149
  All_Types |
blanchet@48200
   150
  Undercover_Types |
blanchet@48183
   151
  Nonmono_Types of strictness * uniformity |
blanchet@52026
   152
  Const_Types of ctr_optim |
blanchet@47768
   153
  No_Types
blanchet@47768
   154
blanchet@47768
   155
datatype type_enc =
blanchet@47768
   156
  Native of order * polymorphism * type_level |
blanchet@47768
   157
  Guards of polymorphism * type_level |
blanchet@47768
   158
  Tags of polymorphism * type_level
blanchet@47768
   159
blanchet@48654
   160
(* not clear whether ATPs prefer to have their negative variables tagged *)
blanchet@48654
   161
val tag_neg_vars = false
blanchet@48654
   162
blanchet@47768
   163
fun is_type_enc_native (Native _) = true
blanchet@47768
   164
  | is_type_enc_native _ = false
blanchet@47768
   165
fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
blanchet@47768
   166
  | is_type_enc_higher_order _ = false
blanchet@47768
   167
blanchet@47768
   168
fun polymorphism_of_type_enc (Native (_, poly, _)) = poly
blanchet@47768
   169
  | polymorphism_of_type_enc (Guards (poly, _)) = poly
blanchet@47768
   170
  | polymorphism_of_type_enc (Tags (poly, _)) = poly
blanchet@47768
   171
blanchet@48131
   172
fun is_type_enc_polymorphic type_enc =
blanchet@54829
   173
  (case polymorphism_of_type_enc type_enc of
blanchet@48131
   174
    Raw_Polymorphic _ => true
blanchet@48131
   175
  | Type_Class_Polymorphic => true
blanchet@54829
   176
  | _ => false)
blanchet@48131
   177
blanchet@48201
   178
fun is_type_enc_mangling type_enc =
blanchet@48201
   179
  polymorphism_of_type_enc type_enc = Mangled_Monomorphic
blanchet@48201
   180
blanchet@47768
   181
fun level_of_type_enc (Native (_, _, level)) = level
blanchet@47768
   182
  | level_of_type_enc (Guards (_, level)) = level
blanchet@47768
   183
  | level_of_type_enc (Tags (_, level)) = level
blanchet@47768
   184
blanchet@48183
   185
fun is_type_level_uniform (Nonmono_Types (_, Non_Uniform)) = false
blanchet@48183
   186
  | is_type_level_uniform Undercover_Types = false
blanchet@48183
   187
  | is_type_level_uniform _ = true
blanchet@47768
   188
blanchet@48183
   189
fun is_type_level_sound (Const_Types _) = false
blanchet@48183
   190
  | is_type_level_sound No_Types = false
blanchet@48183
   191
  | is_type_level_sound _ = true
blanchet@48089
   192
val is_type_enc_sound = is_type_level_sound o level_of_type_enc
blanchet@47768
   193
blanchet@48092
   194
fun is_type_level_monotonicity_based (Nonmono_Types _) = true
blanchet@47768
   195
  | is_type_level_monotonicity_based _ = false
blanchet@47768
   196
blanchet@45516
   197
val no_lamsN = "no_lams" (* used internally; undocumented *)
blanchet@45513
   198
val hide_lamsN = "hide_lams"
blanchet@46365
   199
val liftingN = "lifting"
blanchet@46365
   200
val combsN = "combs"
blanchet@46365
   201
val combs_and_liftingN = "combs_and_lifting"
blanchet@46365
   202
val combs_or_liftingN = "combs_or_lifting"
blanchet@45513
   203
val keep_lamsN = "keep_lams"
blanchet@48144
   204
val lam_liftingN = "lam_lifting" (* legacy FIXME: remove *)
blanchet@44088
   205
blanchet@43085
   206
val bound_var_prefix = "B_"
blanchet@47150
   207
val all_bound_var_prefix = "A_"
blanchet@47150
   208
val exist_bound_var_prefix = "E_"
blanchet@43085
   209
val schematic_var_prefix = "V_"
blanchet@43085
   210
val fixed_var_prefix = "v_"
blanchet@43085
   211
val tvar_prefix = "T_"
blanchet@48219
   212
val tfree_prefix = "tf_"
blanchet@43085
   213
val const_prefix = "c_"
blanchet@48219
   214
val type_const_prefix = "t_"
blanchet@46435
   215
val native_type_prefix = "n_"
blanchet@43085
   216
val class_prefix = "cl_"
blanchet@43085
   217
blanchet@45509
   218
(* Freshness almost guaranteed! *)
blanchet@46392
   219
val atp_prefix = "ATP" ^ Long_Name.separator
blanchet@45509
   220
val atp_weak_prefix = "ATP:"
blanchet@52076
   221
val atp_weak_suffix = ":ATP"
blanchet@45509
   222
blanchet@45554
   223
val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
blanchet@45554
   224
val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
blanchet@45554
   225
val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
blanchet@43907
   226
blanchet@46392
   227
val skolem_const_prefix = atp_prefix ^ "Sko"
blanchet@43085
   228
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
blanchet@43085
   229
val new_skolem_const_prefix = skolem_const_prefix ^ "n"
blanchet@43085
   230
blanchet@45554
   231
val combinator_prefix = "COMB"
blanchet@45554
   232
blanchet@48142
   233
val class_decl_prefix = "cl_"
blanchet@42998
   234
val type_decl_prefix = "ty_"
blanchet@42998
   235
val sym_decl_prefix = "sy_"
blanchet@52004
   236
val datatype_decl_prefix = "dt_"
blanchet@52004
   237
val class_memb_prefix = "cm_"
blanchet@43989
   238
val guards_sym_formula_prefix = "gsy_"
blanchet@44396
   239
val tags_sym_formula_prefix = "tsy_"
blanchet@46409
   240
val uncurried_alias_eq_prefix = "unc_"
blanchet@40204
   241
val fact_prefix = "fact_"
blanchet@38282
   242
val conjecture_prefix = "conj_"
blanchet@38282
   243
val helper_prefix = "help_"
blanchet@48142
   244
val subclass_prefix = "subcl_"
blanchet@48142
   245
val tcon_clause_prefix = "tcon_"
blanchet@43085
   246
val tfree_clause_prefix = "tfree_"
blanchet@38282
   247
blanchet@45554
   248
val lam_fact_prefix = "ATP.lambda_"
blanchet@42881
   249
val typed_helper_suffix = "_T"
blanchet@42881
   250
val untyped_helper_suffix = "_U"
blanchet@42881
   251
blanchet@44491
   252
val predicator_name = "pp"
blanchet@44491
   253
val app_op_name = "aa"
blanchet@44491
   254
val type_guard_name = "gg"
blanchet@44491
   255
val type_tag_name = "tt"
blanchet@42531
   256
blanchet@43174
   257
val prefixed_predicator_name = const_prefix ^ predicator_name
blanchet@43130
   258
val prefixed_app_op_name = const_prefix ^ app_op_name
blanchet@43130
   259
val prefixed_type_tag_name = const_prefix ^ type_tag_name
blanchet@43130
   260
blanchet@43085
   261
(*Escaping of special characters.
blanchet@43085
   262
  Alphanumeric characters are left unchanged.
blanchet@54798
   263
  The character _ goes to __.
blanchet@43085
   264
  Characters in the range ASCII space to / go to _A to _P, respectively.
blanchet@54798
   265
  Other characters go to _nnn where nnn is the decimal ASCII code. *)
blanchet@43093
   266
val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
blanchet@43085
   267
blanchet@43085
   268
fun ascii_of_char c =
blanchet@43085
   269
  if Char.isAlphaNum c then
blanchet@43085
   270
    String.str c
blanchet@43085
   271
  else if c = #"_" then
blanchet@43085
   272
    "__"
blanchet@43085
   273
  else if #" " <= c andalso c <= #"/" then
blanchet@43085
   274
    "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
blanchet@43085
   275
  else
blanchet@43085
   276
    (* fixed width, in case more digits follow *)
blanchet@43085
   277
    "_" ^ stringN_of_int 3 (Char.ord c)
blanchet@43085
   278
blanchet@43085
   279
val ascii_of = String.translate ascii_of_char
blanchet@43085
   280
blanchet@43085
   281
(** Remove ASCII armoring from names in proof files **)
blanchet@43085
   282
blanchet@43085
   283
(* We don't raise error exceptions because this code can run inside a worker
blanchet@43085
   284
   thread. Also, the errors are impossible. *)
blanchet@43085
   285
val unascii_of =
blanchet@43085
   286
  let
blanchet@47975
   287
    fun un rcs [] = String.implode (rev rcs)
blanchet@43085
   288
      | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
blanchet@43085
   289
        (* Three types of _ escapes: __, _A to _P, _nnn *)
blanchet@43496
   290
      | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
blanchet@43085
   291
      | un rcs (#"_" :: c :: cs) =
blanchet@43085
   292
        if #"A" <= c andalso c<= #"P" then
blanchet@43085
   293
          (* translation of #" " to #"/" *)
blanchet@43085
   294
          un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
blanchet@43085
   295
        else
blanchet@43496
   296
          let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
blanchet@54829
   297
            (case Int.fromString (String.implode digits) of
blanchet@43085
   298
              SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
blanchet@54829
   299
            | NONE => un (c :: #"_" :: rcs) cs (* ERROR *))
blanchet@43085
   300
          end
blanchet@43085
   301
      | un rcs (c :: cs) = un (c :: rcs) cs
blanchet@43085
   302
  in un [] o String.explode end
blanchet@43085
   303
blanchet@43085
   304
(* If string s has the prefix s1, return the result of deleting it,
blanchet@43085
   305
   un-ASCII'd. *)
blanchet@45511
   306
fun unprefix_and_unascii s1 s =
blanchet@43085
   307
  if String.isPrefix s1 s then
blanchet@43085
   308
    SOME (unascii_of (String.extract (s, size s1, NONE)))
blanchet@43085
   309
  else
blanchet@43085
   310
    NONE
blanchet@43085
   311
blanchet@43159
   312
val proxy_table =
blanchet@43159
   313
  [("c_False", (@{const_name False}, (@{thm fFalse_def},
blanchet@43159
   314
       ("fFalse", @{const_name ATP.fFalse})))),
blanchet@43159
   315
   ("c_True", (@{const_name True}, (@{thm fTrue_def},
blanchet@43159
   316
       ("fTrue", @{const_name ATP.fTrue})))),
blanchet@43159
   317
   ("c_Not", (@{const_name Not}, (@{thm fNot_def},
blanchet@43159
   318
       ("fNot", @{const_name ATP.fNot})))),
blanchet@43159
   319
   ("c_conj", (@{const_name conj}, (@{thm fconj_def},
blanchet@43159
   320
       ("fconj", @{const_name ATP.fconj})))),
blanchet@43159
   321
   ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
blanchet@43159
   322
       ("fdisj", @{const_name ATP.fdisj})))),
blanchet@43159
   323
   ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
blanchet@43159
   324
       ("fimplies", @{const_name ATP.fimplies})))),
blanchet@43159
   325
   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
nik@43678
   326
       ("fequal", @{const_name ATP.fequal})))),
nik@43678
   327
   ("c_All", (@{const_name All}, (@{thm fAll_def},
nik@43678
   328
       ("fAll", @{const_name ATP.fAll})))),
nik@43678
   329
   ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
nik@43678
   330
       ("fEx", @{const_name ATP.fEx}))))]
blanchet@43085
   331
blanchet@43159
   332
val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
blanchet@43085
   333
blanchet@43085
   334
(* Readable names for the more common symbolic functions. Do not mess with the
blanchet@43085
   335
   table unless you know what you are doing. *)
blanchet@43085
   336
val const_trans_table =
blanchet@54554
   337
  [(@{const_name False}, "False"),
blanchet@43085
   338
   (@{const_name True}, "True"),
blanchet@43085
   339
   (@{const_name Not}, "Not"),
blanchet@43085
   340
   (@{const_name conj}, "conj"),
blanchet@43085
   341
   (@{const_name disj}, "disj"),
blanchet@43085
   342
   (@{const_name implies}, "implies"),
blanchet@43085
   343
   (@{const_name HOL.eq}, "equal"),
nik@43678
   344
   (@{const_name All}, "All"),
nik@43678
   345
   (@{const_name Ex}, "Ex"),
blanchet@43085
   346
   (@{const_name If}, "If"),
blanchet@43085
   347
   (@{const_name Set.member}, "member"),
blanchet@45554
   348
   (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
blanchet@45554
   349
   (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
blanchet@45554
   350
   (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
blanchet@45554
   351
   (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
blanchet@45554
   352
   (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
blanchet@43085
   353
  |> Symtab.make
blanchet@43159
   354
  |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
blanchet@43085
   355
blanchet@43085
   356
(* Invert the table of translations between Isabelle and ATPs. *)
blanchet@43085
   357
val const_trans_table_inv =
blanchet@43085
   358
  const_trans_table |> Symtab.dest |> map swap |> Symtab.make
blanchet@43085
   359
val const_trans_table_unprox =
blanchet@43085
   360
  Symtab.empty
blanchet@43159
   361
  |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
blanchet@43085
   362
blanchet@43085
   363
val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
blanchet@43085
   364
val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
blanchet@43085
   365
blanchet@43085
   366
fun lookup_const c =
blanchet@54829
   367
  (case Symtab.lookup const_trans_table c of
blanchet@43085
   368
    SOME c' => c'
blanchet@54829
   369
  | NONE => ascii_of c)
blanchet@43085
   370
blanchet@43622
   371
fun ascii_of_indexname (v, 0) = ascii_of v
blanchet@43622
   372
  | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
blanchet@43085
   373
blanchet@43085
   374
fun make_bound_var x = bound_var_prefix ^ ascii_of x
blanchet@44403
   375
fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
blanchet@44403
   376
fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
blanchet@43085
   377
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
blanchet@43085
   378
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
blanchet@43085
   379
blanchet@52076
   380
fun make_tvar (s, i) = tvar_prefix ^ ascii_of_indexname (unquote_tvar s, i)
blanchet@52076
   381
fun make_tfree s = tfree_prefix ^ ascii_of (unquote_tvar s)
blanchet@48142
   382
fun tvar_name ((x as (s, _)), _) = (make_tvar x, s)
blanchet@43085
   383
blanchet@45301
   384
(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
nik@44587
   385
local
wenzelm@49323
   386
  val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT
nik@44587
   387
  fun default c = const_prefix ^ lookup_const c
nik@44587
   388
in
nik@44587
   389
  fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
blanchet@47768
   390
    | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _))) c =
blanchet@44754
   391
      if c = choice_const then tptp_choice else default c
nik@44587
   392
    | make_fixed_const _ c = default c
nik@44587
   393
end
blanchet@43085
   394
blanchet@43085
   395
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
blanchet@43085
   396
blanchet@48142
   397
fun make_class clas = class_prefix ^ ascii_of clas
blanchet@43085
   398
blanchet@52031
   399
fun new_skolem_var_name_of_const s =
blanchet@43093
   400
  let val ss = s |> space_explode Long_Name.separator in
blanchet@43093
   401
    nth ss (length ss - 2)
blanchet@43093
   402
  end
blanchet@43093
   403
blanchet@48318
   404
(* These are ignored anyway by the relevance filter (unless they appear in
blanchet@48318
   405
   higher-order places) but not by the monomorphizer. *)
blanchet@48318
   406
val atp_logical_consts =
wenzelm@56245
   407
  [@{const_name Pure.prop}, @{const_name Pure.conjunction},
wenzelm@56245
   408
   @{const_name Pure.all}, @{const_name Pure.imp}, @{const_name Pure.eq},
wenzelm@56245
   409
   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
blanchet@48318
   410
   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
blanchet@48318
   411
blanchet@43248
   412
(* These are either simplified away by "Meson.presimplify" (most of the time) or
blanchet@43248
   413
   handled specially via "fFalse", "fTrue", ..., "fequal". *)
blanchet@43248
   414
val atp_irrelevant_consts =
blanchet@54089
   415
  [@{const_name False}, @{const_name True}, @{const_name Not}, @{const_name conj},
blanchet@54089
   416
   @{const_name disj}, @{const_name implies}, @{const_name HOL.eq}, @{const_name If},
blanchet@54089
   417
   @{const_name Let}]
blanchet@43248
   418
blanchet@48318
   419
val atp_widely_irrelevant_consts = atp_logical_consts @ atp_irrelevant_consts
blanchet@43248
   420
blanchet@54089
   421
val atp_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_irrelevant_consts)
blanchet@54089
   422
val atp_widely_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_widely_irrelevant_consts)
blanchet@54089
   423
blanchet@54089
   424
val is_irrelevant_const = Symtab.defined atp_irrelevant_const_tab
blanchet@54089
   425
val is_widely_irrelevant_const = Symtab.defined atp_widely_irrelevant_const_tab
blanchet@54089
   426
blanchet@43258
   427
fun add_schematic_const (x as (_, T)) =
blanchet@43258
   428
  Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
blanchet@43258
   429
val add_schematic_consts_of =
blanchet@43258
   430
  Term.fold_aterms (fn Const (x as (s, _)) =>
blanchet@48227
   431
                       not (member (op =) atp_widely_irrelevant_consts s)
blanchet@43258
   432
                       ? add_schematic_const x
blanchet@43258
   433
                      | _ => I)
blanchet@43258
   434
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
blanchet@43248
   435
blanchet@48133
   436
val tvar_a_str = "'a"
wenzelm@56254
   437
val tvar_a_z = ((tvar_a_str, 0), @{sort type})
blanchet@48142
   438
val tvar_a = TVar tvar_a_z
blanchet@48142
   439
val tvar_a_name = tvar_name tvar_a_z
blanchet@48133
   440
val itself_name = `make_fixed_type_const @{type_name itself}
wenzelm@56243
   441
val TYPE_name = `(make_fixed_const NONE) @{const_name Pure.type}
blanchet@54820
   442
val tvar_a_atype = AType ((tvar_a_name, []), [])
blanchet@54820
   443
val a_itself_atype = AType ((itself_name, []), [tvar_a_atype])
blanchet@48133
   444
blanchet@43085
   445
(** Definitions and functions for FOL clauses and formulas for TPTP **)
blanchet@43085
   446
blanchet@48142
   447
(** Type class membership **)
blanchet@43263
   448
blanchet@48142
   449
(* In our data structures, [] exceptionally refers to the top class, not to
blanchet@48142
   450
   the empty class. *)
blanchet@44625
   451
blanchet@48142
   452
val class_of_types = the_single @{sort type}
blanchet@43085
   453
blanchet@48142
   454
fun normalize_classes cls = if member (op =) cls class_of_types then [] else cls
blanchet@48142
   455
blanchet@48142
   456
(* Arity of type constructor "s :: (arg1, ..., argN) res" *)
blanchet@48142
   457
fun make_axiom_tcon_clause (s, name, (cl, args)) =
blanchet@43085
   458
  let
blanchet@48142
   459
    val args = args |> map normalize_classes
blanchet@48133
   460
    val tvars =
blanchet@48142
   461
      1 upto length args |> map (fn j => TVar ((tvar_a_str, j), @{sort type}))
blanchet@48142
   462
  in (name, args ~~ tvars, (cl, Type (s, tvars))) end
blanchet@43085
   463
blanchet@43622
   464
(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
blanchet@43622
   465
   theory thy provided its arguments have the corresponding sorts. *)
blanchet@48142
   466
fun class_pairs thy tycons cls =
blanchet@43093
   467
  let
blanchet@43093
   468
    val alg = Sign.classes_of thy
blanchet@43093
   469
    fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
blanchet@48142
   470
    fun add_class tycon cl =
blanchet@48142
   471
      cons (cl, domain_sorts tycon cl)
blanchet@43093
   472
      handle Sorts.CLASS_ERROR _ => I
blanchet@48142
   473
    fun try_classes tycon = (tycon, fold (add_class tycon) cls [])
blanchet@43093
   474
  in map try_classes tycons end
blanchet@43085
   475
blanchet@48141
   476
(* Proving one (tycon, class) membership may require proving others, so
blanchet@48141
   477
   iterate. *)
blanchet@48142
   478
fun all_class_pairs _ _ [] = ([], [])
blanchet@48142
   479
  | all_class_pairs thy tycons cls =
blanchet@48141
   480
    let
blanchet@48141
   481
      fun maybe_insert_class s =
blanchet@54820
   482
        (s <> class_of_types andalso not (member (op =) cls s)) ? insert (op =) s
blanchet@48142
   483
      val pairs = class_pairs thy tycons cls
blanchet@48142
   484
      val new_cls =
blanchet@48142
   485
        [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs
blanchet@48142
   486
      val (cls', pairs') = all_class_pairs thy tycons new_cls
blanchet@48142
   487
    in (cls' @ cls, union (op =) pairs' pairs) end
blanchet@48141
   488
blanchet@51651
   489
fun tcon_clause _ _ [] = []
blanchet@51651
   490
  | tcon_clause seen n ((_, []) :: rest) = tcon_clause seen n rest
blanchet@51651
   491
  | tcon_clause seen n ((tcons, (ar as (cl, _)) :: ars) :: rest) =
blanchet@48142
   492
    if cl = class_of_types then
blanchet@51651
   493
      tcon_clause seen n ((tcons, ars) :: rest)
blanchet@48142
   494
    else if member (op =) seen cl then
blanchet@48142
   495
      (* multiple clauses for the same (tycon, cl) pair *)
blanchet@48142
   496
      make_axiom_tcon_clause (tcons,
blanchet@54820
   497
        lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n, ar) ::
blanchet@51651
   498
      tcon_clause seen (n + 1) ((tcons, ars) :: rest)
blanchet@48141
   499
    else
blanchet@54820
   500
      make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl, ar) ::
blanchet@51651
   501
      tcon_clause (cl :: seen) n ((tcons, ars) :: rest)
blanchet@43085
   502
blanchet@48142
   503
fun make_tcon_clauses thy tycons =
blanchet@51651
   504
  all_class_pairs thy tycons ##> tcon_clause [] 1
blanchet@43085
   505
blanchet@43085
   506
blanchet@43085
   507
(** Isabelle class relations **)
blanchet@43085
   508
blanchet@48142
   509
(* Generate a list ("sub", "supers") such that "sub" is a proper subclass of all
blanchet@48142
   510
   "supers". *)
blanchet@48142
   511
fun make_subclass_pairs thy subs supers =
blanchet@48141
   512
  let
blanchet@48142
   513
    val class_less = curry (Sorts.class_less (Sign.classes_of thy))
blanchet@48142
   514
    fun supers_of sub = (sub, filter (class_less sub) supers)
blanchet@48142
   515
  in map supers_of subs |> filter_out (null o snd) end
blanchet@43085
   516
blanchet@43859
   517
(* intermediate terms *)
blanchet@43859
   518
datatype iterm =
blanchet@48135
   519
  IConst of (string * string) * typ * typ list |
blanchet@48135
   520
  IVar of (string * string) * typ |
blanchet@43859
   521
  IApp of iterm * iterm |
blanchet@48135
   522
  IAbs of ((string * string) * typ) * iterm
blanchet@43085
   523
blanchet@43859
   524
fun ityp_of (IConst (_, T, _)) = T
blanchet@43859
   525
  | ityp_of (IVar (_, T)) = T
blanchet@43859
   526
  | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
blanchet@43859
   527
  | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
blanchet@43085
   528
blanchet@43085
   529
(*gets the head of a combinator application, along with the list of arguments*)
blanchet@43859
   530
fun strip_iterm_comb u =
blanchet@43496
   531
  let
blanchet@43859
   532
    fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
blanchet@43496
   533
      | stripc x = x
blanchet@43496
   534
  in stripc (u, []) end
blanchet@43085
   535
blanchet@45316
   536
fun atomic_types_of T = fold_atyps (insert (op =)) T []
blanchet@43085
   537
blanchet@43085
   538
fun new_skolem_const_name s num_T_args =
blanchet@43085
   539
  [new_skolem_const_prefix, s, string_of_int num_T_args]
wenzelm@46711
   540
  |> Long_Name.implode
blanchet@43085
   541
blanchet@47932
   542
val alpha_to_beta = Logic.varifyT_global @{typ "'a => 'b"}
blanchet@47932
   543
val alpha_to_beta_to_alpha_to_beta = alpha_to_beta --> alpha_to_beta
blanchet@47932
   544
blanchet@44594
   545
fun robust_const_type thy s =
blanchet@45509
   546
  if s = app_op_name then
blanchet@47932
   547
    alpha_to_beta_to_alpha_to_beta
blanchet@45554
   548
  else if String.isPrefix lam_lifted_prefix s then
blanchet@47932
   549
    alpha_to_beta
blanchet@45509
   550
  else
blanchet@45509
   551
    (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
blanchet@45509
   552
    s |> Sign.the_const_type thy
blanchet@44594
   553
blanchet@52038
   554
fun ary_of (Type (@{type_name fun}, [_, T])) = 1 + ary_of T
blanchet@52038
   555
  | ary_of _ = 0
blanchet@46642
   556
blanchet@44594
   557
(* This function only makes sense if "T" is as general as possible. *)
blanchet@51920
   558
fun robust_const_type_args thy (s, T) =
blanchet@45509
   559
  if s = app_op_name then
blanchet@45509
   560
    let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
blanchet@45509
   561
  else if String.isPrefix old_skolem_const_prefix s then
blanchet@45509
   562
    [] |> Term.add_tvarsT T |> rev |> map TVar
blanchet@45554
   563
  else if String.isPrefix lam_lifted_prefix s then
blanchet@45554
   564
    if String.isPrefix lam_lifted_poly_prefix s then
blanchet@45511
   565
      let val (T1, T2) = T |> dest_funT in [T1, T2] end
blanchet@45511
   566
    else
blanchet@45511
   567
      []
blanchet@45509
   568
  else
blanchet@45509
   569
    (s, T) |> Sign.const_typargs thy
blanchet@44594
   570
blanchet@54798
   571
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term. Also accumulates sort
blanchet@54798
   572
   infomation. *)
blanchet@52031
   573
fun iterm_of_term thy type_enc bs (P $ Q) =
blanchet@43085
   574
    let
blanchet@52031
   575
      val (P', P_atomics_Ts) = iterm_of_term thy type_enc bs P
blanchet@52031
   576
      val (Q', Q_atomics_Ts) = iterm_of_term thy type_enc bs Q
blanchet@43859
   577
    in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
blanchet@52031
   578
  | iterm_of_term thy type_enc _ (Const (c, T)) =
blanchet@54798
   579
    (IConst (`(make_fixed_const (SOME type_enc)) c, T, robust_const_type_args thy (c, T)),
blanchet@45316
   580
     atomic_types_of T)
blanchet@54798
   581
  | iterm_of_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of T)
blanchet@52031
   582
  | iterm_of_term _ type_enc _ (Var (v as (s, _), T)) =
blanchet@43085
   583
    (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
blanchet@43085
   584
       let
blanchet@43085
   585
         val Ts = T |> strip_type |> swap |> op ::
blanchet@43085
   586
         val s' = new_skolem_const_name s (length Ts)
blanchet@47768
   587
       in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
blanchet@43085
   588
     else
blanchet@45316
   589
       IVar ((make_schematic_var v, s), T), atomic_types_of T)
blanchet@52031
   590
  | iterm_of_term _ _ bs (Bound j) =
blanchet@45316
   591
    nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
blanchet@52031
   592
  | iterm_of_term thy type_enc bs (Abs (s, T, t)) =
nik@43678
   593
    let
nik@43678
   594
      fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
nik@43678
   595
      val s = vary s
blanchet@44403
   596
      val name = `make_bound_var s
blanchet@52031
   597
      val (tm, atomic_Ts) = iterm_of_term thy type_enc ((s, (name, T)) :: bs) t
blanchet@54798
   598
    in
blanchet@54798
   599
      (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T))
blanchet@54798
   600
    end
blanchet@43085
   601
blanchet@48089
   602
(* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *)
blanchet@44785
   603
val queries = ["?", "_query"]
blanchet@44785
   604
val ats = ["@", "_at"]
blanchet@44785
   605
blanchet@42689
   606
fun try_unsuffixes ss s =
blanchet@42689
   607
  fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
blanchet@42689
   608
blanchet@52031
   609
fun type_enc_of_string strictness s =
blanchet@48131
   610
  (case try (unprefix "tc_") s of
blanchet@54829
   611
    SOME s => (SOME Type_Class_Polymorphic, s)
blanchet@54829
   612
  | NONE =>
blanchet@54829
   613
    (case try (unprefix "poly_") s of
blanchet@54829
   614
      (* It's still unclear whether all TFF1 implementations will support
blanchet@54829
   615
         type signatures such as "!>[A : $tType] : $o", with phantom type
blanchet@54829
   616
         variables. *)
blanchet@54829
   617
      SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
blanchet@54829
   618
    | NONE =>
blanchet@54829
   619
      (case try (unprefix "raw_mono_") s of
blanchet@54829
   620
        SOME s => (SOME Raw_Monomorphic, s)
blanchet@54829
   621
      | NONE =>
blanchet@54829
   622
        (case try (unprefix "mono_") s of
blanchet@54829
   623
          SOME s => (SOME Mangled_Monomorphic, s)
blanchet@54829
   624
        | NONE => (NONE, s)))))
blanchet@48092
   625
  ||> (fn s =>
blanchet@54829
   626
       (case try_unsuffixes queries s of
blanchet@54829
   627
         SOME s =>
blanchet@54829
   628
         (case try_unsuffixes queries s of
blanchet@54829
   629
           SOME s => (Nonmono_Types (strictness, Non_Uniform), s)
blanchet@54829
   630
         | NONE => (Nonmono_Types (strictness, Uniform), s))
blanchet@54829
   631
        | NONE =>
blanchet@54829
   632
          (case try_unsuffixes ats s of
blanchet@54829
   633
            SOME s => (Undercover_Types, s)
blanchet@54829
   634
          | NONE => (All_Types, s))))
blanchet@44768
   635
  |> (fn (poly, (level, core)) =>
blanchet@54829
   636
        (case (core, (poly, level)) of
blanchet@54829
   637
          ("native", (SOME poly, _)) =>
blanchet@54829
   638
          (case (poly, level) of
blanchet@54829
   639
            (Mangled_Monomorphic, _) =>
blanchet@54829
   640
            if is_type_level_uniform level then Native (First_Order, Mangled_Monomorphic, level)
blanchet@54829
   641
            else raise Same.SAME
blanchet@54829
   642
          | (Raw_Monomorphic, _) => raise Same.SAME
blanchet@54829
   643
          | (poly, All_Types) => Native (First_Order, poly, All_Types))
blanchet@54829
   644
        | ("native_higher", (SOME poly, _)) =>
blanchet@54829
   645
          (case (poly, level) of
blanchet@54829
   646
            (_, Nonmono_Types _) => raise Same.SAME
blanchet@54829
   647
          | (_, Undercover_Types) => raise Same.SAME
blanchet@54829
   648
          | (Mangled_Monomorphic, _) =>
blanchet@54829
   649
            if is_type_level_uniform level then
blanchet@54829
   650
              Native (Higher_Order THF_With_Choice, Mangled_Monomorphic, level)
blanchet@54829
   651
            else
blanchet@54829
   652
              raise Same.SAME
blanchet@54829
   653
           | (poly as Raw_Polymorphic _, All_Types) =>
blanchet@54829
   654
             Native (Higher_Order THF_With_Choice, poly, All_Types)
blanchet@54829
   655
           | _ => raise Same.SAME)
blanchet@54829
   656
        | ("guards", (SOME poly, _)) =>
blanchet@54829
   657
          if (poly = Mangled_Monomorphic andalso
blanchet@54829
   658
              level = Undercover_Types) orelse
blanchet@54829
   659
             poly = Type_Class_Polymorphic then
blanchet@54829
   660
            raise Same.SAME
blanchet@54829
   661
          else
blanchet@54829
   662
            Guards (poly, level)
blanchet@54829
   663
        | ("tags", (SOME poly, _)) =>
blanchet@54829
   664
          if (poly = Mangled_Monomorphic andalso
blanchet@54829
   665
              level = Undercover_Types) orelse
blanchet@54829
   666
             poly = Type_Class_Polymorphic then
blanchet@54829
   667
            raise Same.SAME
blanchet@54829
   668
          else
blanchet@54829
   669
            Tags (poly, level)
blanchet@54829
   670
        | ("args", (SOME poly, All_Types (* naja *))) =>
blanchet@54829
   671
          if poly = Type_Class_Polymorphic then raise Same.SAME
blanchet@54829
   672
          else Guards (poly, Const_Types Without_Ctr_Optim)
blanchet@54829
   673
        | ("args", (SOME poly, Nonmono_Types (_, Uniform) (* naja *))) =>
blanchet@54829
   674
          if poly = Mangled_Monomorphic orelse
blanchet@54829
   675
             poly = Type_Class_Polymorphic then
blanchet@54829
   676
            raise Same.SAME
blanchet@54829
   677
          else
blanchet@54829
   678
            Guards (poly, Const_Types With_Ctr_Optim)
blanchet@54829
   679
        | ("erased", (NONE, All_Types (* naja *))) =>
blanchet@54829
   680
          Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
blanchet@54829
   681
        | _ => raise Same.SAME))
blanchet@44785
   682
  handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
blanchet@42613
   683
blanchet@47768
   684
fun adjust_order THF_Without_Choice (Higher_Order _) =
blanchet@47768
   685
    Higher_Order THF_Without_Choice
blanchet@47768
   686
  | adjust_order _ type_enc = type_enc
blanchet@47768
   687
blanchet@48134
   688
fun no_type_classes Type_Class_Polymorphic =
blanchet@48134
   689
    Raw_Polymorphic With_Phantom_Type_Vars
blanchet@48134
   690
  | no_type_classes poly = poly
blanchet@48134
   691
blanchet@54197
   692
fun adjust_type_enc (THF (Polymorphic, choice)) (Native (order, poly, level)) =
blanchet@48134
   693
    Native (adjust_order choice order, no_type_classes poly, level)
blanchet@54197
   694
  | adjust_type_enc (THF (Monomorphic, choice)) (Native (order, _, level)) =
blanchet@48004
   695
    Native (adjust_order choice order, Mangled_Monomorphic, level)
blanchet@52995
   696
  | adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) =
blanchet@47767
   697
    Native (First_Order, Mangled_Monomorphic, level)
blanchet@48131
   698
  | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
blanchet@48131
   699
    Native (First_Order, poly, level)
blanchet@48131
   700
  | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) =
blanchet@47767
   701
    Native (First_Order, Mangled_Monomorphic, level)
blanchet@47767
   702
  | adjust_type_enc (TFF _) (Native (_, poly, level)) =
blanchet@48134
   703
    Native (First_Order, no_type_classes poly, level)
blanchet@47767
   704
  | adjust_type_enc format (Native (_, poly, level)) =
blanchet@48134
   705
    adjust_type_enc format (Guards (no_type_classes poly, level))
blanchet@44416
   706
  | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
blanchet@48089
   707
    (if is_type_enc_sound type_enc then Tags else Guards) stuff
blanchet@44416
   708
  | adjust_type_enc _ type_enc = type_enc
blanchet@43101
   709
blanchet@48302
   710
fun is_lambda_free t =
blanchet@54829
   711
  (case t of
blanchet@48302
   712
    @{const Not} $ t1 => is_lambda_free t1
blanchet@48302
   713
  | Const (@{const_name All}, _) $ Abs (_, _, t') => is_lambda_free t'
blanchet@48302
   714
  | Const (@{const_name All}, _) $ t1 => is_lambda_free t1
blanchet@48302
   715
  | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_lambda_free t'
blanchet@48302
   716
  | Const (@{const_name Ex}, _) $ t1 => is_lambda_free t1
blanchet@48302
   717
  | @{const HOL.conj} $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
blanchet@48302
   718
  | @{const HOL.disj} $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
blanchet@48302
   719
  | @{const HOL.implies} $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
blanchet@46818
   720
  | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
blanchet@48302
   721
    is_lambda_free t1 andalso is_lambda_free t2
blanchet@54829
   722
  | _ => not (exists_subterm (fn Abs _ => true | _ => false) t))
blanchet@46818
   723
blanchet@46818
   724
fun simple_translate_lambdas do_lambdas ctxt t =
blanchet@48302
   725
  if is_lambda_free t then
blanchet@46818
   726
    t
blanchet@46818
   727
  else
blanchet@46818
   728
    let
blanchet@46818
   729
      fun trans Ts t =
blanchet@54829
   730
        (case t of
blanchet@46818
   731
          @{const Not} $ t1 => @{const Not} $ trans Ts t1
blanchet@46818
   732
        | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
blanchet@46818
   733
          t0 $ Abs (s, T, trans (T :: Ts) t')
blanchet@54829
   734
        | (t0 as Const (@{const_name All}, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
blanchet@46818
   735
        | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
blanchet@46818
   736
          t0 $ Abs (s, T, trans (T :: Ts) t')
blanchet@54829
   737
        | (t0 as Const (@{const_name Ex}, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
blanchet@54829
   738
        | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
blanchet@54829
   739
        | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
blanchet@54829
   740
        | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
blanchet@54829
   741
        | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) $ t1 $ t2 =>
blanchet@46818
   742
          t0 $ trans Ts t1 $ trans Ts t2
blanchet@46818
   743
        | _ =>
blanchet@46818
   744
          if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
blanchet@54829
   745
          else t |> Envir.eta_contract |> do_lambdas ctxt Ts)
blanchet@46818
   746
      val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
blanchet@46818
   747
    in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
blanchet@46818
   748
blanchet@46818
   749
fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
blanchet@46818
   750
    do_cheaply_conceal_lambdas Ts t1
blanchet@46818
   751
    $ do_cheaply_conceal_lambdas Ts t2
blanchet@46818
   752
  | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
blanchet@46818
   753
    Const (lam_lifted_poly_prefix ^ serial_string (),
blanchet@46818
   754
           T --> fastype_of1 (T :: Ts, t))
blanchet@46818
   755
  | do_cheaply_conceal_lambdas _ t = t
blanchet@46818
   756
blanchet@46818
   757
fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
blanchet@46818
   758
fun conceal_bounds Ts t =
blanchet@46818
   759
  subst_bounds (map (Free o apfst concealed_bound_name)
blanchet@46818
   760
                    (0 upto length Ts - 1 ~~ Ts), t)
blanchet@46818
   761
fun reveal_bounds Ts =
blanchet@46818
   762
  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
blanchet@46818
   763
                    (0 upto length Ts - 1 ~~ Ts))
blanchet@46818
   764
blanchet@46818
   765
fun do_introduce_combinators ctxt Ts t =
blanchet@46818
   766
  let val thy = Proof_Context.theory_of ctxt in
blanchet@46818
   767
    t |> conceal_bounds Ts
blanchet@46818
   768
      |> cterm_of thy
blanchet@46818
   769
      |> Meson_Clausify.introduce_combinators_in_cterm
blanchet@46818
   770
      |> prop_of |> Logic.dest_equals |> snd
blanchet@46818
   771
      |> reveal_bounds Ts
blanchet@46818
   772
  end
blanchet@46818
   773
  (* A type variable of sort "{}" will make abstraction fail. *)
blanchet@46818
   774
  handle THM _ => t |> do_cheaply_conceal_lambdas Ts
blanchet@46818
   775
val introduce_combinators = simple_translate_lambdas do_introduce_combinators
blanchet@46818
   776
blanchet@45509
   777
fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
blanchet@45509
   778
  | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
blanchet@45509
   779
  | constify_lifted (Free (x as (s, _))) =
blanchet@45554
   780
    (if String.isPrefix lam_lifted_prefix s then Const else Free) x
blanchet@45509
   781
  | constify_lifted t = t
blanchet@45509
   782
blanchet@45554
   783
fun lift_lams_part_1 ctxt type_enc =
blanchet@49982
   784
  map hol_close_form #> rpair ctxt
blanchet@44088
   785
  #-> Lambda_Lifting.lift_lambdas
blanchet@48131
   786
          (SOME ((if is_type_enc_polymorphic type_enc then
blanchet@45564
   787
                    lam_lifted_poly_prefix
blanchet@45564
   788
                  else
blanchet@45564
   789
                    lam_lifted_mono_prefix) ^ "_a"))
blanchet@44088
   790
          Lambda_Lifting.is_quantifier
blanchet@45554
   791
  #> fst
blanchet@46818
   792
blanchet@46818
   793
fun lift_lams_part_2 ctxt (facts, lifted) =
blanchet@46818
   794
  (facts, lifted)
blanchet@52125
   795
  (* Lambda-lifting sometimes leaves some lambdas around; we need some way to
blanchet@52125
   796
     get rid of them *)
blanchet@46818
   797
  |> pairself (map (introduce_combinators ctxt))
blanchet@46818
   798
  |> pairself (map constify_lifted)
blanchet@47718
   799
  (* Requires bound variables not to clash with any schematic variables (as
blanchet@47718
   800
     should be the case right after lambda-lifting). *)
blanchet@49982
   801
  |>> map (hol_open_form (unprefix hol_close_form_prefix))
blanchet@49982
   802
  ||> map (hol_open_form I)
blanchet@46818
   803
blanchet@46818
   804
fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
blanchet@44088
   805
blanchet@44088
   806
fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
blanchet@44088
   807
    intentionalize_def t
blanchet@44088
   808
  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
blanchet@44088
   809
    let
blanchet@44088
   810
      fun lam T t = Abs (Name.uu, T, t)
blanchet@44088
   811
      val (head, args) = strip_comb t ||> rev
blanchet@44088
   812
      val head_T = fastype_of head
blanchet@44088
   813
      val n = length args
blanchet@44088
   814
      val arg_Ts = head_T |> binder_types |> take n |> rev
blanchet@44088
   815
      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
blanchet@44088
   816
    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
blanchet@44088
   817
  | intentionalize_def t = t
blanchet@44088
   818
blanchet@47981
   819
type ifact =
blanchet@43496
   820
  {name : string,
blanchet@46340
   821
   stature : stature,
blanchet@53586
   822
   role : atp_formula_role,
blanchet@53586
   823
   iformula : (string * string, typ, iterm, string * string) atp_formula,
blanchet@43496
   824
   atomic_types : typ list}
blanchet@38282
   825
blanchet@47981
   826
fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) =
blanchet@54798
   827
  {name = name, stature = stature, role = role, iformula = f iformula, atomic_types = atomic_types}
blanchet@54798
   828
  : ifact
blanchet@42542
   829
blanchet@47981
   830
fun ifact_lift f ({iformula, ...} : ifact) = f iformula
blanchet@42558
   831
blanchet@47150
   832
fun insert_type thy get_T x xs =
blanchet@43064
   833
  let val T = get_T x in
blanchet@47150
   834
    if exists (type_instance thy T o get_T) xs then xs
blanchet@47150
   835
    else x :: filter_out (type_generalization thy T o get_T) xs
blanchet@43064
   836
  end
blanchet@42677
   837
blanchet@48202
   838
fun chop_fun 0 T = ([], T)
blanchet@48202
   839
  | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
blanchet@48202
   840
    chop_fun (n - 1) ran_T |>> cons dom_T
blanchet@48202
   841
  | chop_fun _ T = ([], T)
blanchet@41136
   842
blanchet@52032
   843
fun filter_type_args thy ctrss type_enc s ary T_args =
blanchet@45315
   844
  let val poly = polymorphism_of_type_enc type_enc in
blanchet@50968
   845
    if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *)
blanchet@48202
   846
      T_args
blanchet@54829
   847
    else
blanchet@54829
   848
      (case type_enc of
blanchet@54829
   849
        Native (_, Raw_Polymorphic _, _) => T_args
blanchet@54829
   850
      | Native (_, Type_Class_Polymorphic, _) => T_args
blanchet@54829
   851
      | _ =>
blanchet@54829
   852
        let
blanchet@54829
   853
          fun gen_type_args _ _ [] = []
blanchet@54829
   854
            | gen_type_args keep strip_ty T_args =
blanchet@54829
   855
              let
blanchet@54829
   856
                val U = robust_const_type thy s
blanchet@54829
   857
                val (binder_Us, body_U) = strip_ty U
blanchet@54829
   858
                val in_U_vars = fold Term.add_tvarsT binder_Us []
blanchet@54829
   859
                val out_U_vars = Term.add_tvarsT body_U []
blanchet@54829
   860
                fun filt (U_var, T) =
blanchet@54829
   861
                  if keep (member (op =) in_U_vars U_var,
blanchet@54829
   862
                           member (op =) out_U_vars U_var) then
blanchet@54829
   863
                    T
blanchet@54829
   864
                  else
blanchet@54829
   865
                    dummyT
blanchet@54829
   866
                val U_args = (s, U) |> robust_const_type_args thy
blanchet@54829
   867
              in map (filt o apfst dest_TVar) (U_args ~~ T_args) end
blanchet@54829
   868
              handle TYPE _ => T_args
blanchet@54829
   869
          fun is_always_ctr (s', T') =
blanchet@54829
   870
            s' = s andalso type_equiv thy (T', robust_const_type thy s')
blanchet@54829
   871
          val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary)
blanchet@54829
   872
          val ctr_infer_type_args = gen_type_args fst strip_type
blanchet@54829
   873
          val level = level_of_type_enc type_enc
blanchet@54829
   874
        in
blanchet@54829
   875
          if level = No_Types orelse s = @{const_name HOL.eq} orelse
blanchet@54829
   876
             (case level of Const_Types _ => s = app_op_name | _ => false) then
blanchet@54829
   877
            []
blanchet@54829
   878
          else if poly = Mangled_Monomorphic then
blanchet@54829
   879
            T_args
blanchet@54829
   880
          else if level = All_Types then
blanchet@54829
   881
            (case type_enc of
blanchet@54829
   882
              Guards _ => noninfer_type_args T_args
blanchet@54829
   883
            | Tags _ => [])
blanchet@54829
   884
          else if level = Undercover_Types then
blanchet@54829
   885
            noninfer_type_args T_args
blanchet@54829
   886
          else if level <> Const_Types Without_Ctr_Optim andalso
blanchet@54829
   887
                  exists (exists is_always_ctr) ctrss then
blanchet@54829
   888
            ctr_infer_type_args T_args
blanchet@54829
   889
          else
blanchet@54829
   890
            T_args
blanchet@54829
   891
        end)
blanchet@44774
   892
  end
blanchet@42227
   893
blanchet@46338
   894
val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
blanchet@44594
   895
val fused_infinite_type = Type (fused_infinite_type_name, [])
blanchet@44594
   896
blanchet@54820
   897
fun raw_atp_type_of_typ type_enc =
blanchet@42994
   898
  let
blanchet@42994
   899
    fun term (Type (s, Ts)) =
blanchet@54820
   900
      AType ((case (is_type_enc_higher_order type_enc, s) of
blanchet@48138
   901
               (true, @{type_name bool}) => `I tptp_bool_type
blanchet@48138
   902
             | (true, @{type_name fun}) => `I tptp_fun_type
blanchet@54820
   903
             | _ =>
blanchet@54820
   904
               if s = fused_infinite_type_name andalso is_type_enc_native type_enc then
blanchet@54820
   905
                 `I tptp_individual_type
blanchet@54820
   906
               else
blanchet@54820
   907
                 `make_fixed_type_const s, []), map term Ts)
blanchet@54820
   908
    | term (TFree (s, _)) = AType ((`make_tfree s, []), [])
blanchet@55212
   909
    | term (TVar z) = AType ((tvar_name z, []), [])
blanchet@42994
   910
  in term end
blanchet@42562
   911
blanchet@54820
   912
fun atp_term_of_atp_type (AType ((name, _), tys)) = ATerm ((name, []), map atp_term_of_atp_type tys)
blanchet@54820
   913
  | atp_term_of_atp_type _ = raise Fail "unexpected type"
blanchet@48138
   914
blanchet@54820
   915
fun atp_type_of_type_arg type_enc T =
blanchet@54820
   916
  if T = dummyT then NONE else SOME (raw_atp_type_of_typ type_enc T)
blanchet@43401
   917
blanchet@42562
   918
(* This shouldn't clash with anything else. *)
blanchet@46409
   919
val uncurried_alias_sep = "\000"
blanchet@46392
   920
val mangled_type_sep = "\001"
blanchet@46392
   921
blanchet@46409
   922
val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
blanchet@42542
   923
blanchet@54820
   924
fun generic_mangled_type_name f (AType ((name, _), [])) = f name
blanchet@54820
   925
  | generic_mangled_type_name f (AType ((name, _), tys)) =
blanchet@54820
   926
    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) ^ ")"
blanchet@48138
   927
  | generic_mangled_type_name _ _ = raise Fail "unexpected type"
blanchet@42542
   928
blanchet@54820
   929
fun mangled_type type_enc = generic_mangled_type_name fst o raw_atp_type_of_typ type_enc
blanchet@44396
   930
blanchet@46435
   931
fun make_native_type s =
blanchet@54820
   932
  if s = tptp_bool_type orelse s = tptp_fun_type orelse s = tptp_individual_type then s
blanchet@54820
   933
  else native_type_prefix ^ ascii_of s
blanchet@43085
   934
blanchet@54820
   935
fun native_atp_type_of_raw_atp_type type_enc pred_sym ary =
blanchet@42963
   936
  let
blanchet@44593
   937
    fun to_mangled_atype ty =
blanchet@54820
   938
      AType (((make_native_type (generic_mangled_type_name fst ty),
blanchet@54820
   939
               generic_mangled_type_name snd ty), []), [])
blanchet@54820
   940
    fun to_poly_atype (AType ((name, clss), tys)) = AType ((name, clss), map to_poly_atype tys)
blanchet@48138
   941
      | to_poly_atype _ = raise Fail "unexpected type"
blanchet@44593
   942
    val to_atype =
blanchet@48131
   943
      if is_type_enc_polymorphic type_enc then to_poly_atype
blanchet@44593
   944
      else to_mangled_atype
blanchet@42963
   945
    fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
blanchet@42998
   946
    fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
blanchet@48138
   947
      | to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
blanchet@48138
   948
      | to_fo _ _ = raise Fail "unexpected type"
blanchet@54820
   949
    fun to_ho (ty as AType (((s, _), _), tys)) =
nik@43676
   950
        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
blanchet@48138
   951
      | to_ho _ = raise Fail "unexpected type"
blanchet@43626
   952
  in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
blanchet@42963
   953
blanchet@54820
   954
fun native_atp_type_of_typ type_enc pred_sym ary =
blanchet@54820
   955
  native_atp_type_of_raw_atp_type type_enc pred_sym ary o raw_atp_type_of_typ type_enc
blanchet@42963
   956
blanchet@48133
   957
(* Make atoms for sorted type variables. *)
blanchet@48133
   958
fun generic_add_sorts_on_type _ [] = I
blanchet@48133
   959
  | generic_add_sorts_on_type T (s :: ss) =
blanchet@48133
   960
    generic_add_sorts_on_type T ss
blanchet@48142
   961
    #> (if s = the_single @{sort type} then I else insert (op =) (s, T))
blanchet@48133
   962
fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S
blanchet@48133
   963
  | add_sorts_on_tfree _ = I
blanchet@48133
   964
fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S
blanchet@48133
   965
  | add_sorts_on_tvar _ = I
blanchet@48133
   966
blanchet@48133
   967
fun process_type_args type_enc T_args =
blanchet@48133
   968
  if is_type_enc_native type_enc then
blanchet@54820
   969
    (map (native_atp_type_of_typ type_enc false 0) T_args, [])
blanchet@48133
   970
  else
blanchet@54820
   971
    ([], map_filter (Option.map atp_term_of_atp_type o atp_type_of_type_arg type_enc) T_args)
blanchet@48133
   972
blanchet@48142
   973
fun class_atom type_enc (cl, T) =
blanchet@48133
   974
  let
blanchet@48142
   975
    val cl = `make_class cl
blanchet@48133
   976
    val (ty_args, tm_args) = process_type_args type_enc [T]
blanchet@48133
   977
    val tm_args =
blanchet@48133
   978
      tm_args @
blanchet@48133
   979
      (case type_enc of
blanchet@54820
   980
        Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
blanchet@54820
   981
        [ATerm ((TYPE_name, ty_args), [])]
blanchet@54820
   982
      | _ => [])
blanchet@48142
   983
  in AAtom (ATerm ((cl, ty_args), tm_args)) end
blanchet@48142
   984
blanchet@48142
   985
fun class_atoms type_enc (cls, T) =
blanchet@48142
   986
  map (fn cl => class_atom type_enc (cl, T)) cls
blanchet@48142
   987
blanchet@51998
   988
fun class_membs_of_types type_enc add_sorts_on_typ Ts =
blanchet@54798
   989
  [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
blanchet@48133
   990
blanchet@48141
   991
fun mk_aconns c = split_last #> uncurry (fold_rev (mk_aconn c))
blanchet@48133
   992
blanchet@48133
   993
fun mk_ahorn [] phi = phi
blanchet@48133
   994
  | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
blanchet@48133
   995
blanchet@48133
   996
fun mk_aquant _ [] phi = phi
blanchet@48133
   997
  | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
blanchet@48133
   998
    if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
blanchet@48133
   999
  | mk_aquant q xs phi = AQuant (q, xs, phi)
blanchet@48133
  1000
blanchet@48133
  1001
fun mk_atyquant _ [] phi = phi
blanchet@48133
  1002
  | mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) =
blanchet@48133
  1003
    if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi)
blanchet@48133
  1004
  | mk_atyquant q xs phi = ATyQuant (q, xs, phi)
blanchet@48133
  1005
blanchet@48133
  1006
fun close_universally add_term_vars phi =
blanchet@48133
  1007
  let
blanchet@48133
  1008
    fun add_formula_vars bounds (ATyQuant (_, _, phi)) =
blanchet@48133
  1009
        add_formula_vars bounds phi
blanchet@48133
  1010
      | add_formula_vars bounds (AQuant (_, xs, phi)) =
blanchet@48133
  1011
        add_formula_vars (map fst xs @ bounds) phi
blanchet@48133
  1012
      | add_formula_vars bounds (AConn (_, phis)) =
blanchet@48133
  1013
        fold (add_formula_vars bounds) phis
blanchet@48133
  1014
      | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
blanchet@50706
  1015
  in mk_aquant AForall (rev (add_formula_vars [] phi [])) phi end
blanchet@48133
  1016
blanchet@48133
  1017
fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
blanchet@48133
  1018
    (if is_tptp_variable s andalso
blanchet@48133
  1019
        not (String.isPrefix tvar_prefix s) andalso
blanchet@48133
  1020
        not (member (op =) bounds name) then
blanchet@48133
  1021
       insert (op =) (name, NONE)
blanchet@48133
  1022
     else
blanchet@48133
  1023
       I)
blanchet@48133
  1024
    #> fold (add_term_vars bounds) tms
blanchet@48133
  1025
  | add_term_vars bounds (AAbs (((name, _), tm), args)) =
blanchet@48133
  1026
    add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
blanchet@50706
  1027
blanchet@48133
  1028
fun close_formula_universally phi = close_universally add_term_vars phi
blanchet@48133
  1029
blanchet@48133
  1030
fun add_iterm_vars bounds (IApp (tm1, tm2)) =
blanchet@48133
  1031
    fold (add_iterm_vars bounds) [tm1, tm2]
blanchet@48133
  1032
  | add_iterm_vars _ (IConst _) = I
blanchet@48133
  1033
  | add_iterm_vars bounds (IVar (name, T)) =
blanchet@48133
  1034
    not (member (op =) bounds name) ? insert (op =) (name, SOME T)
blanchet@48133
  1035
  | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
blanchet@48133
  1036
blanchet@46409
  1037
fun aliased_uncurried ary (s, s') =
blanchet@46409
  1038
  (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
blanchet@46409
  1039
fun unaliased_uncurried (s, s') =
blanchet@54829
  1040
  (case space_explode uncurried_alias_sep s of
blanchet@46392
  1041
    [_] => (s, s')
blanchet@46392
  1042
  | [s1, s2] => (s1, unsuffix s2 s')
blanchet@54829
  1043
  | _ => raise Fail "ill-formed explicit application alias")
blanchet@46392
  1044
blanchet@46392
  1045
fun raw_mangled_const_name type_name ty_args (s, s') =
blanchet@42963
  1046
  let
blanchet@42963
  1047
    fun type_suffix f g =
blanchet@46392
  1048
      fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
blanchet@46392
  1049
               ty_args ""
blanchet@42963
  1050
  in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
blanchet@47768
  1051
fun mangled_const_name type_enc =
blanchet@54820
  1052
  map_filter (atp_type_of_type_arg type_enc)
blanchet@46392
  1053
  #> raw_mangled_const_name generic_mangled_type_name
blanchet@42542
  1054
blanchet@42542
  1055
val parse_mangled_ident =
blanchet@42542
  1056
  Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
blanchet@42542
  1057
blanchet@42542
  1058
fun parse_mangled_type x =
blanchet@42542
  1059
  (parse_mangled_ident
blanchet@42542
  1060
   -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
blanchet@48132
  1061
                    [] >> (ATerm o apfst (rpair []))) x
blanchet@42542
  1062
and parse_mangled_types x =
blanchet@42542
  1063
  (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
blanchet@42542
  1064
blanchet@42542
  1065
fun unmangled_type s =
blanchet@42542
  1066
  s |> suffix ")" |> raw_explode
blanchet@42542
  1067
    |> Scan.finite Symbol.stopper
blanchet@42542
  1068
           (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
blanchet@42542
  1069
                                                quote s)) parse_mangled_type))
blanchet@42542
  1070
    |> fst
blanchet@42542
  1071
blanchet@46392
  1072
fun unmangled_const_name s =
blanchet@46409
  1073
  (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
blanchet@51920
  1074
blanchet@42542
  1075
fun unmangled_const s =
blanchet@46392
  1076
  let val ss = unmangled_const_name s in
blanchet@42542
  1077
    (hd ss, map unmangled_type (tl ss))
blanchet@42542
  1078
  end
blanchet@42542
  1079
blanchet@51920
  1080
val unmangled_invert_const = invert_const o hd o unmangled_const_name
blanchet@51920
  1081
blanchet@44773
  1082
fun introduce_proxies_in_iterm type_enc =
blanchet@42568
  1083
  let
blanchet@43987
  1084
    fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
blanchet@43987
  1085
      | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
blanchet@43987
  1086
                       _ =
blanchet@43987
  1087
        (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
blanchet@43987
  1088
           limitation. This works in conjuction with special code in
blanchet@43987
  1089
           "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
blanchet@43987
  1090
           possible. *)
blanchet@43987
  1091
        IAbs ((`I "P", p_T),
blanchet@43987
  1092
              IApp (IConst (`I ho_quant, T, []),
blanchet@43987
  1093
                    IAbs ((`I "X", x_T),
blanchet@43987
  1094
                          IApp (IConst (`I "P", p_T, []),
blanchet@43987
  1095
                                IConst (`I "X", x_T, [])))))
blanchet@43987
  1096
      | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
blanchet@43987
  1097
    fun intro top_level args (IApp (tm1, tm2)) =
blanchet@43987
  1098
        IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
blanchet@43987
  1099
      | intro top_level args (IConst (name as (s, _), T, T_args)) =
blanchet@42570
  1100
        (case proxify_const s of
blanchet@54829
  1101
          SOME proxy_base =>
blanchet@54829
  1102
          if top_level orelse is_type_enc_higher_order type_enc then
blanchet@54829
  1103
            (case (top_level, s) of
blanchet@54829
  1104
              (_, "c_False") => IConst (`I tptp_false, T, [])
blanchet@54829
  1105
            | (_, "c_True") => IConst (`I tptp_true, T, [])
blanchet@54829
  1106
            | (false, "c_Not") => IConst (`I tptp_not, T, [])
blanchet@54829
  1107
            | (false, "c_conj") => IConst (`I tptp_and, T, [])
blanchet@54829
  1108
            | (false, "c_disj") => IConst (`I tptp_or, T, [])
blanchet@54829
  1109
            | (false, "c_implies") => IConst (`I tptp_implies, T, [])
blanchet@54829
  1110
            | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
blanchet@54829
  1111
            | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
blanchet@54829
  1112
            | (false, s) =>
blanchet@54829
  1113
              if is_tptp_equal s then
blanchet@54829
  1114
                if length args = 2 then
blanchet@54829
  1115
                  IConst (`I tptp_equal, T, [])
blanchet@54829
  1116
                else
blanchet@54829
  1117
                  (* Eta-expand partially applied THF equality, because the
blanchet@54829
  1118
                     LEO-II and Satallax parsers complain about not being able to
blanchet@54829
  1119
                     infer the type of "=". *)
blanchet@54829
  1120
                  let val i_T = domain_type T in
blanchet@54829
  1121
                    IAbs ((`I "Y", i_T),
blanchet@54829
  1122
                          IAbs ((`I "Z", i_T),
blanchet@54829
  1123
                                IApp (IApp (IConst (`I tptp_equal, T, []),
blanchet@54829
  1124
                                            IConst (`I "Y", i_T, [])),
blanchet@54829
  1125
                                      IConst (`I "Z", i_T, []))))
blanchet@54829
  1126
                  end
blanchet@54829
  1127
              else
blanchet@54829
  1128
                IConst (name, T, [])
blanchet@54829
  1129
            | _ => IConst (name, T, []))
blanchet@54829
  1130
          else
blanchet@54829
  1131
            IConst (proxy_base |>> prefix const_prefix, T, T_args)
blanchet@54829
  1132
         | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
blanchet@54829
  1133
                   else IConst (name, T, T_args))
blanchet@43987
  1134
      | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
blanchet@43987
  1135
      | intro _ _ tm = tm
blanchet@43987
  1136
  in intro true [] end
blanchet@42568
  1137
blanchet@47768
  1138
fun mangle_type_args_in_const type_enc (name as (s, _)) T_args =
blanchet@48203
  1139
  if String.isPrefix const_prefix s andalso is_type_enc_mangling type_enc then
blanchet@48203
  1140
    (mangled_const_name type_enc T_args name, [])
blanchet@48203
  1141
  else
blanchet@48203
  1142
    (name, T_args)
blanchet@47768
  1143
fun mangle_type_args_in_iterm type_enc =
blanchet@48201
  1144
  if is_type_enc_mangling type_enc then
blanchet@44774
  1145
    let
blanchet@44774
  1146
      fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
blanchet@44774
  1147
        | mangle (tm as IConst (_, _, [])) = tm
blanchet@46392
  1148
        | mangle (IConst (name, T, T_args)) =
blanchet@47768
  1149
          mangle_type_args_in_const type_enc name T_args
blanchet@46392
  1150
          |> (fn (name, T_args) => IConst (name, T, T_args))
blanchet@44774
  1151
        | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
blanchet@44774
  1152
        | mangle tm = tm
blanchet@44774
  1153
    in mangle end
blanchet@44774
  1154
  else
blanchet@44774
  1155
    I
blanchet@44774
  1156
blanchet@52032
  1157
fun filter_type_args_in_const _ _ _ _ _ [] = []
blanchet@52032
  1158
  | filter_type_args_in_const thy ctrss type_enc ary s T_args =
blanchet@54829
  1159
    (case unprefix_and_unascii const_prefix s of
blanchet@54829
  1160
      NONE => if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then [] else T_args
blanchet@54829
  1161
    | SOME s'' => filter_type_args thy ctrss type_enc (unmangled_invert_const s'') ary T_args)
blanchet@52029
  1162
blanchet@52028
  1163
fun filter_type_args_in_iterm thy ctrss type_enc =
blanchet@38282
  1164
  let
blanchet@44774
  1165
    fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
blanchet@44774
  1166
      | filt ary (IConst (name as (s, _), T, T_args)) =
blanchet@52032
  1167
        filter_type_args_in_const thy ctrss type_enc ary s T_args
blanchet@46392
  1168
        |> (fn T_args => IConst (name, T, T_args))
blanchet@44774
  1169
      | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
blanchet@44774
  1170
      | filt _ tm = tm
blanchet@44774
  1171
  in filt 0 end
blanchet@44773
  1172
blanchet@52031
  1173
fun iformula_of_prop ctxt type_enc iff_for_eq =
blanchet@44773
  1174
  let
blanchet@44773
  1175
    val thy = Proof_Context.theory_of ctxt
blanchet@45316
  1176
    fun do_term bs t atomic_Ts =
blanchet@52031
  1177
      iterm_of_term thy type_enc bs (Envir.eta_contract t)
blanchet@44773
  1178
      |>> (introduce_proxies_in_iterm type_enc
blanchet@47768
  1179
           #> mangle_type_args_in_iterm type_enc #> AAtom)
blanchet@45316
  1180
      ||> union (op =) atomic_Ts
blanchet@44403
  1181
    fun do_quant bs q pos s T t' =
blanchet@44403
  1182
      let
blanchet@44403
  1183
        val s = singleton (Name.variant_list (map fst bs)) s
blanchet@44403
  1184
        val universal = Option.map (q = AExists ? not) pos
blanchet@44403
  1185
        val name =
blanchet@44403
  1186
          s |> `(case universal of
blanchet@44403
  1187
                   SOME true => make_all_bound_var
blanchet@44403
  1188
                 | SOME false => make_exist_bound_var
blanchet@44403
  1189
                 | NONE => make_bound_var)
blanchet@44403
  1190
      in
blanchet@44403
  1191
        do_formula ((s, (name, T)) :: bs) pos t'
blanchet@44403
  1192
        #>> mk_aquant q [(name, SOME T)]
blanchet@45316
  1193
        ##> union (op =) (atomic_types_of T)
blanchet@38518
  1194
      end
blanchet@44403
  1195
    and do_conn bs c pos1 t1 pos2 t2 =
blanchet@44403
  1196
      do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
blanchet@44403
  1197
    and do_formula bs pos t =
blanchet@54829
  1198
      (case t of
blanchet@44403
  1199
        @{const Trueprop} $ t1 => do_formula bs pos t1
blanchet@44403
  1200
      | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
blanchet@54829
  1201
      | Const (@{const_name All}, _) $ Abs (s, T, t') => do_quant bs AForall pos s T t'
blanchet@45167
  1202
      | (t0 as Const (@{const_name All}, _)) $ t1 =>
blanchet@45167
  1203
        do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
blanchet@54829
  1204
      | Const (@{const_name Ex}, _) $ Abs (s, T, t') => do_quant bs AExists pos s T t'
blanchet@45167
  1205
      | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
blanchet@45167
  1206
        do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
blanchet@44403
  1207
      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
blanchet@44403
  1208
      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
blanchet@54829
  1209
      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies (Option.map not pos) t1 pos t2
haftmann@38864
  1210
      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
blanchet@47905
  1211
        if iff_for_eq then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
blanchet@54829
  1212
      | _ => do_term bs t)
blanchet@38282
  1213
  in do_formula [] end
blanchet@38282
  1214
wenzelm@51717
  1215
fun presimplify_term ctxt t =
blanchet@47151
  1216
  if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
wenzelm@51717
  1217
    t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
wenzelm@51717
  1218
      |> Meson.presimplify ctxt
blanchet@47151
  1219
      |> prop_of
blanchet@47151
  1220
  else
blanchet@47151
  1221
    t
blanchet@38282
  1222
blanchet@45514
  1223
fun preprocess_abstractions_in_terms trans_lams facts =
blanchet@43862
  1224
  let
blanchet@43863
  1225
    val (facts, lambda_ts) =
blanchet@45514
  1226
      facts |> map (snd o snd) |> trans_lams
blanchet@47975
  1227
            |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
blanchet@45554
  1228
    val lam_facts =
blanchet@43863
  1229
      map2 (fn t => fn j =>
blanchet@48438
  1230
               ((lam_fact_prefix ^ Int.toString j,
blanchet@48438
  1231
                 (Global, Non_Rec_Def)), (Axiom, t)))
blanchet@43863
  1232
           lambda_ts (1 upto length lambda_ts)
blanchet@45554
  1233
  in (facts, lam_facts) end
blanchet@38282
  1234
blanchet@38282
  1235
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
blanchet@42353
  1236
   same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
blanchet@38282
  1237
fun freeze_term t =
blanchet@38282
  1238
  let
blanchet@52076
  1239
    (* Freshness is desirable for completeness, but not for soundness. *)
blanchet@52076
  1240
    fun indexed_name (s, i) = s ^ "_" ^ string_of_int i ^ atp_weak_suffix
blanchet@44814
  1241
    fun freeze (t $ u) = freeze t $ freeze u
blanchet@44814
  1242
      | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
blanchet@52076
  1243
      | freeze (Var (x, T)) = Free (indexed_name x, T)
blanchet@44814
  1244
      | freeze t = t
blanchet@52076
  1245
    fun freeze_tvar (x, S) = TFree (indexed_name x, S)
blanchet@52076
  1246
  in
blanchet@52076
  1247
    t |> exists_subterm is_Var t ? freeze
blanchet@52076
  1248
      |> exists_type (exists_subtype is_TVar) t
blanchet@52076
  1249
         ? map_types (map_type_tvar freeze_tvar)
blanchet@52076
  1250
  end
blanchet@38282
  1251
blanchet@47769
  1252
fun presimp_prop ctxt type_enc t =
blanchet@47713
  1253
  let
blanchet@47713
  1254
    val thy = Proof_Context.theory_of ctxt
blanchet@47713
  1255
    val t = t |> Envir.beta_eta_contract
blanchet@47713
  1256
              |> transform_elim_prop
blanchet@47713
  1257
              |> Object_Logic.atomize_term thy
blanchet@47713
  1258
    val need_trueprop = (fastype_of t = @{typ bool})
blanchet@47913
  1259
    val is_ho = is_type_enc_higher_order type_enc
blanchet@47713
  1260
  in
blanchet@47713
  1261
    t |> need_trueprop ? HOLogic.mk_Trueprop
blanchet@47954
  1262
      |> (if is_ho then unextensionalize_def
blanchet@47954
  1263
          else cong_extensionalize_term thy #> abs_extensionalize_term ctxt)
wenzelm@51717
  1264
      |> presimplify_term ctxt
blanchet@47713
  1265
      |> HOLogic.dest_Trueprop
blanchet@47713
  1266
  end
blanchet@47713
  1267
  handle TERM _ => @{const True}
blanchet@43096
  1268
blanchet@55212
  1269
(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
blanchet@55212
  1270
   reasons. *)
blanchet@47905
  1271
fun should_use_iff_for_eq CNF _ = false
blanchet@47905
  1272
  | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
blanchet@47905
  1273
  | should_use_iff_for_eq _ _ = true
blanchet@47905
  1274
blanchet@47975
  1275
fun make_formula ctxt format type_enc iff_for_eq name stature role t =
blanchet@43096
  1276
  let
blanchet@47905
  1277
    val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
blanchet@45316
  1278
    val (iformula, atomic_Ts) =
blanchet@52031
  1279
      iformula_of_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t []
blanchet@48144
  1280
      |>> close_universally add_iterm_vars
blanchet@38282
  1281
  in
blanchet@47975
  1282
    {name = name, stature = stature, role = role, iformula = iformula,
blanchet@45316
  1283
     atomic_types = atomic_Ts}
blanchet@38282
  1284
  end
blanchet@38282
  1285
blanchet@54197
  1286
fun is_format_with_defs (THF _) = true
blanchet@48004
  1287
  | is_format_with_defs _ = false
blanchet@48004
  1288
blanchet@47971
  1289
fun make_fact ctxt format type_enc iff_for_eq
blanchet@47971
  1290
              ((name, stature as (_, status)), t) =
blanchet@47971
  1291
  let
blanchet@47971
  1292
    val role =
blanchet@48438
  1293
      if is_format_with_defs format andalso status = Non_Rec_Def andalso
blanchet@47991
  1294
         is_legitimate_tptp_def t then
blanchet@47971
  1295
        Definition
blanchet@47971
  1296
      else
blanchet@47971
  1297
        Axiom
blanchet@47971
  1298
  in
blanchet@54829
  1299
    (case t |> make_formula ctxt format type_enc iff_for_eq name stature role of
blanchet@47971
  1300
      formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
blanchet@47971
  1301
      if s = tptp_true then NONE else SOME formula
blanchet@54829
  1302
    | formula => SOME formula)
blanchet@47971
  1303
  end
blanchet@42561
  1304
blanchet@44773
  1305
fun make_conjecture ctxt format type_enc =
blanchet@47975
  1306
  map (fn ((name, stature), (role, t)) =>
blanchet@47981
  1307
          let
blanchet@47981
  1308
            val role =
blanchet@55212
  1309
              if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role
blanchet@47981
  1310
          in
blanchet@47981
  1311
            t |> role = Conjecture ? s_not
blanchet@47981
  1312
              |> make_formula ctxt format type_enc true name stature role
blanchet@47981
  1313
          end)
blanchet@38282
  1314
blanchet@42682
  1315
(** Finite and infinite type inference **)
blanchet@42682
  1316
blanchet@48200
  1317
fun tvar_footprint thy s ary =
blanchet@45511
  1318
  (case unprefix_and_unascii const_prefix s of
blanchet@54829
  1319
    SOME s =>
blanchet@54829
  1320
    let fun tvars_of T = [] |> Term.add_tvarsT T |> map fst in
blanchet@54829
  1321
      s |> unmangled_invert_const |> robust_const_type thy |> chop_fun ary |> fst |> map tvars_of
blanchet@54829
  1322
    end
blanchet@54829
  1323
  | NONE => [])
blanchet@44814
  1324
  handle TYPE _ => []
blanchet@44814
  1325
blanchet@48200
  1326
fun type_arg_cover thy pos s ary =
blanchet@45948
  1327
  if is_tptp_equal s then
blanchet@48186
  1328
    if pos = SOME false then [] else 0 upto ary - 1
blanchet@45948
  1329
  else
blanchet@45948
  1330
    let
blanchet@48200
  1331
      val footprint = tvar_footprint thy s ary
blanchet@45948
  1332
      val eq = (s = @{const_name HOL.eq})
blanchet@48080
  1333
      fun cover _ [] = []
blanchet@48080
  1334
        | cover seen ((i, tvars) :: args) =
blanchet@48080
  1335
          cover (union (op =) seen tvars) args
blanchet@45948
  1336
          |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
blanchet@45948
  1337
             ? cons i
blanchet@45948
  1338
    in
blanchet@45948
  1339
      if forall null footprint then
blanchet@45948
  1340
        []
blanchet@45948
  1341
      else
blanchet@45948
  1342
        0 upto length footprint - 1 ~~ footprint
blanchet@45948
  1343
        |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
blanchet@48080
  1344
        |> cover []
blanchet@45948
  1345
    end
blanchet@44814
  1346
blanchet@44399
  1347
type monotonicity_info =
blanchet@44399
  1348
  {maybe_finite_Ts : typ list,
blanchet@44399
  1349
   surely_infinite_Ts : typ list,
blanchet@44399
  1350
   maybe_nonmono_Ts : typ list}
blanchet@44399
  1351
blanchet@44397
  1352
(* These types witness that the type classes they belong to allow infinite
blanchet@44397
  1353
   models and hence that any types with these type classes is monotonic. *)
blanchet@44397
  1354
val known_infinite_types =
blanchet@44634
  1355
  [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
blanchet@44397
  1356
blanchet@46301
  1357
fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
blanchet@46301
  1358
  strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
blanchet@42886
  1359
blanchet@42682
  1360
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
blanchet@42682
  1361
   dangerous because their "exhaust" properties can easily lead to unsound ATP
blanchet@42682
  1362
   proofs. On the other hand, all HOL infinite types can be given the same
blanchet@50969
  1363
   models in first-order logic (via Loewenheim-Skolem). *)
blanchet@42682
  1364
blanchet@48200
  1365
fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
blanchet@48203
  1366
                             maybe_nonmono_Ts}
blanchet@48183
  1367
                       (Nonmono_Types (strictness, _)) T =
blanchet@47150
  1368
    let val thy = Proof_Context.theory_of ctxt in
blanchet@47150
  1369
      (exists (type_intersect thy T) maybe_nonmono_Ts andalso
blanchet@47150
  1370
       not (exists (type_instance thy T) surely_infinite_Ts orelse
blanchet@47150
  1371
            (not (member (type_equiv thy) maybe_finite_Ts T) andalso
blanchet@47150
  1372
             is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
blanchet@47150
  1373
                                             T)))
blanchet@47150
  1374
    end
blanchet@48200
  1375
  | should_encode_type _ _ level _ =
blanchet@48200
  1376
    (level = All_Types orelse level = Undercover_Types)
blanchet@42682
  1377
blanchet@44768
  1378
fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
blanchet@44811
  1379
    should_guard_var () andalso should_encode_type ctxt mono level T
blanchet@44399
  1380
  | should_guard_type _ _ _ _ _ = false
blanchet@42682
  1381
blanchet@48200
  1382
fun is_maybe_universal_name s =
blanchet@48200
  1383
  String.isPrefix bound_var_prefix s orelse
blanchet@48200
  1384
  String.isPrefix all_bound_var_prefix s
blanchet@48200
  1385
blanchet@48200
  1386
fun is_maybe_universal_var (IConst ((s, _), _, _)) = is_maybe_universal_name s
blanchet@44403
  1387
  | is_maybe_universal_var (IVar _) = true
blanchet@44403
  1388
  | is_maybe_universal_var _ = false
blanchet@42836
  1389
blanchet@45947
  1390
datatype site =
blanchet@43361
  1391
  Top_Level of bool option |
blanchet@43361
  1392
  Eq_Arg of bool option |
blanchet@48146
  1393
  Arg of string * int * int |
blanchet@43361
  1394
  Elsewhere
blanchet@42829
  1395
blanchet@45949
  1396
fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
blanchet@45949
  1397
  | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
blanchet@48146
  1398
    let val thy = Proof_Context.theory_of ctxt in
blanchet@54829
  1399
      (case level of
blanchet@48183
  1400
        Nonmono_Types (_, Non_Uniform) =>
blanchet@48146
  1401
        (case (site, is_maybe_universal_var u) of
blanchet@54829
  1402
          (Eq_Arg pos, true) =>
blanchet@54829
  1403
          (pos <> SOME false orelse tag_neg_vars) andalso should_encode_type ctxt mono level T
blanchet@54829
  1404
        | _ => false)
blanchet@48183
  1405
      | Undercover_Types =>
blanchet@48183
  1406
        (case (site, is_maybe_universal_var u) of
blanchet@54829
  1407
          (Eq_Arg pos, true) => pos <> SOME false
blanchet@54829
  1408
        | (Arg (s, j, ary), true) => member (op =) (type_arg_cover thy NONE s ary) j
blanchet@54829
  1409
        | _ => false)
blanchet@54829
  1410
      | _ => should_encode_type ctxt mono level T)
blanchet@48146
  1411
    end
blanchet@45949
  1412
  | should_tag_with_type _ _ _ _ _ _ = false
blanchet@42682
  1413
blanchet@44594
  1414
fun fused_type ctxt mono level =
blanchet@42994
  1415
  let
blanchet@44399
  1416
    val should_encode = should_encode_type ctxt mono level
blanchet@44594
  1417
    fun fuse 0 T = if should_encode T then T else fused_infinite_type
blanchet@44594
  1418
      | fuse ary (Type (@{type_name fun}, [T1, T2])) =
blanchet@44594
  1419
        fuse 0 T1 --> fuse (ary - 1) T2
blanchet@44594
  1420
      | fuse _ _ = raise Fail "expected function type"
blanchet@44594
  1421
  in fuse end
blanchet@42682
  1422
blanchet@44450
  1423
(** predicators and application operators **)
blanchet@41313
  1424
blanchet@42574
  1425
type sym_info =
blanchet@44829
  1426
  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
blanchet@44829
  1427
   in_conj : bool}
blanchet@42563
  1428
blanchet@44829
  1429
fun default_sym_tab_entries type_enc =
blanchet@44829
  1430
  (make_fixed_const NONE @{const_name undefined},
blanchet@54829
  1431
     {pred_sym = false, min_ary = 0, max_ary = 0, types = [], in_conj = false}) ::
blanchet@44829
  1432
  ([tptp_false, tptp_true]
blanchet@54829
  1433
   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @
blanchet@44829
  1434
  ([tptp_equal, tptp_old_equal]
blanchet@54829
  1435
   |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false}))
blanchet@44829
  1436
  |> not (is_type_enc_higher_order type_enc)
blanchet@54829
  1437
    ? cons (prefixed_predicator_name,
blanchet@54829
  1438
      {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false})
blanchet@44829
  1439
blanchet@47073
  1440
datatype app_op_level =
blanchet@47073
  1441
  Min_App_Op |
blanchet@47073
  1442
  Sufficient_App_Op |
blanchet@47073
  1443
  Sufficient_App_Op_And_Predicator |
blanchet@47073
  1444
  Full_App_Op_And_Predicator
blanchet@46389
  1445
blanchet@47932
  1446
fun add_iterm_syms_to_sym_table ctxt app_op_level conj_fact =
blanchet@42558
  1447
  let
blanchet@46642
  1448
    val thy = Proof_Context.theory_of ctxt
blanchet@44772
  1449
    fun consider_var_ary const_T var_T max_ary =
blanchet@43064
  1450
      let
blanchet@43064
  1451
        fun iter ary T =
blanchet@54829
  1452
          if ary = max_ary orelse type_instance thy var_T T orelse type_instance thy T var_T then
blanchet@43210
  1453
            ary
blanchet@43210
  1454
          else
blanchet@43210
  1455
            iter (ary + 1) (range_type T)
blanchet@43064
  1456
      in iter 0 const_T end
blanchet@44403
  1457
    fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
blanchet@47073
  1458
      if (app_op_level = Sufficient_App_Op andalso can dest_funT T) orelse
blanchet@47073
  1459
         (app_op_level = Sufficient_App_Op_And_Predicator andalso
blanchet@47073
  1460
          (can dest_funT T orelse T = @{typ bool})) then
blanchet@43201
  1461
        let
blanchet@47073
  1462
          val bool_vars' =
blanchet@47073
  1463
            bool_vars orelse
blanchet@54829
  1464
            (app_op_level = Sufficient_App_Op_And_Predicator andalso body_type T = @{typ bool})
blanchet@44829
  1465
          fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
blanchet@43201
  1466
            {pred_sym = pred_sym andalso not bool_vars',
blanchet@44772
  1467
             min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
blanchet@44829
  1468
             max_ary = max_ary, types = types, in_conj = in_conj}
blanchet@54829
  1469
          val fun_var_Ts' = fun_var_Ts |> can dest_funT T ? insert_type thy I T
blanchet@43201
  1470
        in
blanchet@54829
  1471
          if bool_vars' = bool_vars andalso pointer_eq (fun_var_Ts', fun_var_Ts) then accum
blanchet@54829
  1472
          else ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
blanchet@43201
  1473
        end
blanchet@43201
  1474
      else
blanchet@43201
  1475
        accum
blanchet@54829
  1476
    fun add_iterm_syms top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
blanchet@47932
  1477
      let val (head, args) = strip_iterm_comb tm in
blanchet@47932
  1478
        (case head of
blanchet@54829
  1479
          IConst ((s, _), T, _) =>
blanchet@54829
  1480
          if is_maybe_universal_name s then
blanchet@54829
  1481
            add_universal_var T accum
blanchet@54829
  1482
          else if String.isPrefix exist_bound_var_prefix s then
blanchet@54829
  1483
            accum
blanchet@54829
  1484
          else
blanchet@54829
  1485
            let val ary = length args in
blanchet@54829
  1486
              ((bool_vars, fun_var_Ts),
blanchet@54829
  1487
               (case Symtab.lookup sym_tab s of
blanchet@54829
  1488
                 SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
blanchet@54829
  1489
                 let
blanchet@54829
  1490
                   val pred_sym = pred_sym andalso top_level andalso not bool_vars
blanchet@54829
  1491
                   val types' = types |> insert_type thy I T
blanchet@54829
  1492
                   val in_conj = in_conj orelse conj_fact
blanchet@54829
  1493
                   val min_ary =
blanchet@54829
  1494
                     if (app_op_level = Sufficient_App_Op orelse
blanchet@54829
  1495
                         app_op_level = Sufficient_App_Op_And_Predicator)
blanchet@54829
  1496
                        andalso not (pointer_eq (types', types)) then
blanchet@54829
  1497
                       fold (consider_var_ary T) fun_var_Ts min_ary
blanchet@54829
  1498
                     else
blanchet@54829
  1499
                       min_ary
blanchet@54829
  1500
                 in
blanchet@54829
  1501
                   Symtab.update (s, {pred_sym = pred_sym, min_ary = Int.min (ary, min_ary),
blanchet@54829
  1502
                     max_ary = Int.max (ary, max_ary), types = types', in_conj = in_conj}) sym_tab
blanchet@54829
  1503
                 end
blanchet@54829
  1504
               | NONE =>
blanchet@54829
  1505
                 let
blanchet@54829
  1506
                   val max_ary =
blanchet@54829
  1507
                     (case unprefix_and_unascii const_prefix s of
blanchet@54829
  1508
                       SOME s =>
blanchet@54829
  1509
                       (if String.isSubstring uncurried_alias_sep s then
blanchet@54829
  1510
                          ary
blanchet@54829
  1511
                        else
blanchet@54829
  1512
                          (case try (ary_of o robust_const_type thy o unmangled_invert_const) s of
blanchet@54829
  1513
                            SOME ary0 => Int.min (ary0, ary)
blanchet@54829
  1514
                          | NONE => ary))
blanchet@54829
  1515
                     | NONE => ary)
blanchet@54829
  1516
                   val pred_sym = top_level andalso max_ary = ary andalso not bool_vars
blanchet@54829
  1517
                   val min_ary =
blanchet@54829
  1518
                     (case app_op_level of
blanchet@54829
  1519
                       Min_App_Op => max_ary
blanchet@54829
  1520
                     | Full_App_Op_And_Predicator => 0
blanchet@54829
  1521
                     | _ => fold (consider_var_ary T) fun_var_Ts max_ary)
blanchet@54829
  1522
                 in
blanchet@54829
  1523
                   Symtab.update_new (s, {pred_sym = pred_sym, min_ary = min_ary, max_ary = max_ary,
blanchet@54829
  1524
                     types = [T], in_conj = conj_fact}) sym_tab
blanchet@54829
  1525
                 end))
blanchet@54829
  1526
            end
blanchet@54829
  1527
        | IVar (_, T) => add_universal_var T accum
blanchet@54829
  1528
        | IAbs ((_, T), tm) => accum |> add_universal_var T |> add_iterm_syms false tm
blanchet@54829
  1529
        | _ => accum)
blanchet@47932
  1530
        |> fold (add_iterm_syms false) args
blanchet@47932
  1531
      end
blanchet@47932
  1532
  in add_iterm_syms end
blanchet@47932
  1533
blanchet@51998
  1534
fun sym_table_of_facts ctxt type_enc app_op_level conjs facts =
blanchet@47932
  1535
  let
blanchet@54829
  1536
    fun add_iterm_syms conj_fact = add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
blanchet@54829
  1537
    fun add_fact_syms conj_fact = ifact_lift (formula_fold NONE (K (add_iterm_syms conj_fact)))
blanchet@44829
  1538
  in
blanchet@44829
  1539
    ((false, []), Symtab.empty)
blanchet@44829
  1540
    |> fold (add_fact_syms true) conjs
blanchet@44829
  1541
    |> fold (add_fact_syms false) facts
blanchet@47932
  1542
    ||> fold Symtab.update (default_sym_tab_entries type_enc)
blanchet@44829
  1543
  end
blanchet@38282
  1544
blanchet@44772
  1545
fun min_ary_of sym_tab s =
blanchet@54829
  1546
  (case Symtab.lookup sym_tab s of
blanchet@42574
  1547
    SOME ({min_ary, ...} : sym_info) => min_ary
blanchet@42558
  1548
  | NONE =>
blanchet@54829
  1549
    (case unprefix_and_unascii const_prefix s of
blanchet@42547
  1550
      SOME s =>
blanchet@51920
  1551
      let val s = s |> unmangled_invert_const in
blanchet@42966
  1552
        if s = predicator_name then 1
blanchet@42966
  1553
        else if s = app_op_name then 2
blanchet@44396
  1554
        else if s = type_guard_name then 1
blanchet@42557
  1555
        else 0
blanchet@42547
  1556
      end
blanchet@54829
  1557
    | NONE => 0))
blanchet@38282
  1558
blanchet@38282
  1559
(* True if the constant ever appears outside of the top-level position in
blanchet@38282
  1560
   literals, or if it appears with different arities (e.g., because of different
blanchet@38282
  1561
   type instantiations). If false, the constant always receives all of its
blanchet@38282
  1562
   arguments and is used as a predicate. *)
blanchet@42558
  1563
fun is_pred_sym sym_tab s =
blanchet@54829
  1564
  (case Symtab.lookup sym_tab s of
blanchet@54829
  1565
    SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => pred_sym andalso min_ary = max_ary
blanchet@54829
  1566
  | NONE => false)
blanchet@38282
  1567
blanchet@54829
  1568
val fTrue_iconst = IConst ((const_prefix ^ "fTrue", @{const_name ATP.fTrue}), @{typ bool}, [])
blanchet@54829
  1569
val predicator_iconst = IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
blanchet@42542
  1570
blanchet@48143
  1571
fun predicatify completish tm =
blanchet@48143
  1572
  if completish then
blanchet@54829
  1573
    IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm), fTrue_iconst)
blanchet@47946
  1574
  else
blanchet@47946
  1575
    IApp (predicator_iconst, tm)
blanchet@47946
  1576
blanchet@47946
  1577
val app_op = `(make_fixed_const NONE) app_op_name
blanchet@47946
  1578
blanchet@43859
  1579
fun list_app head args = fold (curry (IApp o swap)) args head
blanchet@42544
  1580
blanchet@47768
  1581
fun mk_app_op type_enc head arg =
blanchet@42544
  1582
  let
blanchet@46392
  1583
    val head_T = ityp_of head
blanchet@46392
  1584
    val (arg_T, res_T) = dest_funT head_T
blanchet@46392
  1585
    val app =
blanchet@46392
  1586
      IConst (app_op, head_T --> head_T, [arg_T, res_T])
blanchet@47768
  1587
      |> mangle_type_args_in_iterm type_enc
blanchet@46392
  1588
  in list_app app [head, arg] end
blanchet@46392
  1589
blanchet@52038
  1590
fun firstorderize_fact thy ctrss type_enc uncurried_aliases completish sym_tab =
blanchet@46392
  1591
  let
blanchet@47768
  1592
    fun do_app arg head = mk_app_op type_enc head arg
blanchet@51921
  1593
    fun list_app_ops (head, args) = fold do_app args head
blanchet@44773
  1594
    fun introduce_app_ops tm =
blanchet@46392
  1595
      let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
blanchet@54829
  1596
        (case head of
blanchet@46392
  1597
          IConst (name as (s, _), T, T_args) =>
blanchet@51921
  1598
          let
blanchet@51921
  1599
            val min_ary = min_ary_of sym_tab s
blanchet@51921
  1600
            val ary =
blanchet@51921
  1601
              if uncurried_aliases andalso String.isPrefix const_prefix s then
blanchet@51921
  1602
                let
blanchet@51921
  1603
                  val ary = length args
blanchet@51921
  1604
                  (* In polymorphic native type encodings, it is impossible to
blanchet@52038
  1605
                     declare a fully polymorphic symbol that takes more
blanchet@52038
  1606
                     arguments than its signature (even though such concrete
blanchet@52038
  1607
                     instances, where a type variable is instantiated by a
blanchet@52038
  1608
                     function type, are possible.) *)
blanchet@51921
  1609
                  val official_ary =
blanchet@51921
  1610
                    if is_type_enc_polymorphic type_enc then
blanchet@54829
  1611
                      (case unprefix_and_unascii const_prefix s of
blanchet@51921
  1612
                        SOME s' =>
blanchet@54829
  1613
                        (case try (ary_of o robust_const_type thy) (invert_const s') of
blanchet@54829
  1614
                          SOME ary => ary
blanchet@54829
  1615
                        | NONE => min_ary)
blanchet@54829
  1616
                      | NONE => min_ary)
blanchet@51921
  1617
                    else
blanchet@51921
  1618
                      1000000000 (* irrealistically big arity *)
blanchet@51921
  1619
                in Int.min (ary, official_ary) end
blanchet@51921
  1620
              else
blanchet@51921
  1621
                min_ary
blanchet@51921
  1622
            val head =
blanchet@54829
  1623
              if ary = min_ary then head else IConst (aliased_uncurried ary name, T, T_args)
blanchet@51921
  1624
          in
blanchet@51921
  1625
            args |> chop ary |>> list_app head |> list_app_ops
blanchet@51921
  1626
          end
blanchet@54829
  1627
        | _ => list_app_ops (head, args))
blanchet@46392
  1628
      end
blanchet@44773
  1629
    fun introduce_predicators tm =
blanchet@54829
  1630
      (case strip_iterm_comb tm of
blanchet@44773
  1631
        (IConst ((s, _), _, _), _) =>
blanchet@48143
  1632
        if is_pred_sym sym_tab s then tm else predicatify completish tm
blanchet@54829
  1633
      | _ => predicatify completish tm)
blanchet@44773
  1634
    val do_iterm =
blanchet@54829
  1635
      not (is_type_enc_higher_order type_enc) ? (introduce_app_ops #> introduce_predicators)
blanchet@52028
  1636
      #> filter_type_args_in_iterm thy ctrss type_enc
blanchet@44773
  1637
  in update_iformula (formula_map do_iterm) end
blanchet@42573
  1638
blanchet@42573
  1639
(** Helper facts **)
blanchet@42573
  1640
blanchet@44450
  1641
val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
blanchet@44450
  1642
val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
blanchet@44450
  1643
blanchet@43194
  1644
(* The Boolean indicates that a fairly sound type encoding is needed. *)
blanchet@47946
  1645
val base_helper_table =
blanchet@48438
  1646
  [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]),
blanchet@48438
  1647
   (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]),
blanchet@48438
  1648
   (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]),
blanchet@48438
  1649
   (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]),
blanchet@48438
  1650
   (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]),
blanchet@47946
  1651
   ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
blanchet@47946
  1652
   (("fFalse", false), [(General, not_ffalse)]),
blanchet@47946
  1653
   (("fFalse", true), [(General, @{thm True_or_False})]),
blanchet@47946
  1654
   (("fTrue", false), [(General, ftrue)]),
blanchet@47946
  1655
   (("fTrue", true), [(General, @{thm True_or_False})]),
blanchet@47946
  1656
   (("If", true),
blanchet@48438
  1657
    [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}),
blanchet@47946
  1658
     (General, @{thm True_or_False})])]
blanchet@47946
  1659
blanchet@43085
  1660
val helper_table =
blanchet@47946
  1661
  base_helper_table @
blanchet@47946
  1662
  [(("fNot", false),
blanchet@43194
  1663
    @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
blanchet@47946
  1664
           fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
blanchet@48438
  1665
    |> map (pair Non_Rec_Def)),
blanchet@43194
  1666
   (("fconj", false),
blanchet@54829
  1667
    @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" by (unfold fconj_def) fast+}
blanchet@47946
  1668
    |> map (pair General)),
blanchet@43194
  1669
   (("fdisj", false),
blanchet@54829
  1670
    @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" by (unfold fdisj_def) fast+}
blanchet@47946
  1671
    |> map (pair General)),
blanchet@43194
  1672
   (("fimplies", false),
blanchet@43210
  1673
    @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
blanchet@47946
  1674
        by (unfold fimplies_def) fast+}
blanchet@47946
  1675
    |> map (pair General)),
nik@43678
  1676
   (("fequal", true),
nik@43678
  1677
    (* This is a lie: Higher-order equality doesn't need a sound type encoding.
nik@43678
  1678
       However, this is done so for backward compatibility: Including the
nik@43678
  1679
       equality helpers by default in Metis breaks a few existing proofs. *)
nik@43678
  1680
    @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
blanchet@47946
  1681
           fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
blanchet@47946
  1682
    |> map (pair General)),
blanchet@44003
  1683
   (* Partial characterization of "fAll" and "fEx". A complete characterization
blanchet@44003
  1684
      would require the axiom of choice for replay with Metis. *)
blanchet@54829
  1685
   (("fAll", false), [(General, @{lemma "~ fAll P | P x" by (auto simp: fAll_def)})]),
blanchet@54829
  1686
   (("fEx", false), [(General, @{lemma "~ P x | fEx P" by (auto simp: fEx_def)})])]
blanchet@47946
  1687
  |> map (apsnd (map (apsnd zero_var_indexes)))
blanchet@47946
  1688
blanchet@48143
  1689
val completish_helper_table =
blanchet@52071
  1690
  helper_table @
blanchet@47946
  1691
  [((predicator_name, true),
blanchet@47946
  1692
    @{thms True_or_False fTrue_ne_fFalse} |> map (pair General)),
blanchet@47946
  1693
   ((app_op_name, true),
blanchet@52071
  1694
    [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast}),
blanchet@52071
  1695
     (General, @{lemma "EX p. (p x <-> p y) --> x = y" by blast})]),
blanchet@54829
  1696
   (("fconj", false), @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
blanchet@54829
  1697
   (("fdisj", false), @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
blanchet@47946
  1698
   (("fimplies", false),
blanchet@47946
  1699
    @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
blanchet@48438
  1700
    |> map (pair Non_Rec_Def)),
blanchet@47946
  1701
   (("fequal", false),
blanchet@48438
  1702
    (@{thms fequal_table} |> map (pair Non_Rec_Def)) @
blanchet@47946
  1703
    (@{thms fequal_laws} |> map (pair General))),
blanchet@54829
  1704
   (("fAll", false), @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)),
blanchet@54829
  1705
   (("fEx", false), @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))]
blanchet@47946
  1706
  |> map (apsnd (map (apsnd zero_var_indexes)))
blanchet@43085
  1707
blanchet@45920
  1708
fun bound_tvars type_enc sorts Ts =
blanchet@54798
  1709
  (case filter is_TVar Ts of
blanchet@48133
  1710
    [] => I
blanchet@48133
  1711
  | Ts =>
blanchet@54798
  1712
    ((sorts andalso polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic)
blanchet@54798
  1713
     ? mk_ahorn (Ts
blanchet@54798
  1714
       |> class_membs_of_types type_enc add_sorts_on_tvar
blanchet@54798
  1715
       |> map (class_atom type_enc)))
blanchet@48139
  1716
    #> (case type_enc of
blanchet@54798
  1717
         Native (_, poly, _) =>
blanchet@54798
  1718
         mk_atyquant AForall (map (fn TVar (z as (_, S)) =>
blanchet@54820
  1719
           (AType ((tvar_name z, []), []),
blanchet@54820
  1720
            if poly = Type_Class_Polymorphic then map (`make_class) (normalize_classes S)
blanchet@54820
  1721
            else [])) Ts)
blanchet@54798
  1722
        | _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts)))
blanchet@44404
  1723
blanchet@46392
  1724
fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
blanchet@44404
  1725
  (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
blanchet@48132
  1726
   else AAtom (ATerm ((`I tptp_equal, []), [tm1, tm2])))
blanchet@46392
  1727
  |> mk_aquant AForall bounds
blanchet@45377
  1728
  |> close_formula_universally
blanchet@45920
  1729
  |> bound_tvars type_enc true atomic_Ts
blanchet@44404
  1730
blanchet@46406
  1731
val helper_rank = default_rank
blanchet@46406
  1732
val min_rank = 9 * helper_rank div 10
blanchet@46406
  1733
val max_rank = 4 * min_rank
blanchet@46406
  1734
blanchet@46406
  1735
fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n
blanchet@46406
  1736
nik@44495
  1737
val type_tag = `(make_fixed_const NONE) type_tag_name
blanchet@43130
  1738
blanchet@47946
  1739
fun could_specialize_helpers type_enc =
blanchet@54829
  1740
  not (is_type_enc_polymorphic type_enc) andalso level_of_type_enc type_enc <> No_Types
blanchet@52071
  1741
blanchet@47946
  1742
fun should_specialize_helper type_enc t =
blanchet@54829
  1743
  could_specialize_helpers type_enc andalso not (null (Term.hidden_polymorphism t))
blanchet@43159
  1744
blanchet@51998
  1745
fun add_helper_facts_of_sym ctxt format type_enc completish
blanchet@51998
  1746
                            (s, {types, ...} : sym_info) =
blanchet@54829
  1747
  (case unprefix_and_unascii const_prefix s of
blanchet@42573
  1748
    SOME mangled_s =>
blanchet@42573
  1749
    let
blanchet@42573
  1750
      val thy = Proof_Context.theory_of ctxt
blanchet@46392
  1751
      val unmangled_s = mangled_s |> unmangled_const_name |> hd
blanchet@48089
  1752
      fun dub needs_sound j k =
blanchet@47946
  1753
        ascii_of unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
blanchet@46339
  1754
        (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
blanchet@48089
  1755
        (if needs_sound then typed_helper_suffix else untyped_helper_suffix)
blanchet@47932
  1756
      fun specialize_helper t T =
blanchet@47932
  1757
        if unmangled_s = app_op_name then
blanchet@54829
  1758
          let val tyenv = Sign.typ_match thy (alpha_to_beta, domain_type T) Vartab.empty in
blanchet@54829
  1759
            monomorphic_term tyenv t
blanchet@54829
  1760
          end
blanchet@47932
  1761
        else
blanchet@47932
  1762
          specialize_type thy (invert_const unmangled_s, T) t
blanchet@48089
  1763
      fun dub_and_inst needs_sound ((status, t), j) =
blanchet@47932
  1764
        (if should_specialize_helper type_enc t then
blanchet@47946
  1765
           map_filter (try (specialize_helper t)) types
blanchet@47932
  1766
         else
blanchet@47932
  1767
           [t])
blanchet@46339
  1768
        |> tag_list 1
blanchet@48089
  1769
        |> map (fn (k, t) => ((dub needs_sound j k, (Global, status)), t))
blanchet@43860
  1770
      val make_facts = map_filter (make_fact ctxt format type_enc false)
blanchet@48089
  1771
      val sound = is_type_enc_sound type_enc
blanchet@47946
  1772
      val could_specialize = could_specialize_helpers type_enc
blanchet@42573
  1773
    in
blanchet@48089
  1774
      fold (fn ((helper_s, needs_sound), ths) =>
blanchet@48089
  1775
               if (needs_sound andalso not sound) orelse
blanchet@47946
  1776
                  (helper_s <> unmangled_s andalso
blanchet@48143
  1777
                   (not completish orelse could_specialize)) then
blanchet@47810
  1778
                 I
blanchet@47810
  1779
               else
blanchet@47810
  1780
                 ths ~~ (1 upto length ths)
blanchet@48089
  1781
                 |> maps (dub_and_inst needs_sound o apfst (apsnd prop_of))
blanchet@47810
  1782
                 |> make_facts
blanchet@47810
  1783
                 |> union (op = o pairself #iformula))
blanchet@48143
  1784
           (if completish then completish_helper_table else helper_table)
blanchet@42573
  1785
    end
blanchet@54829
  1786
  | NONE => I)
blanchet@51998
  1787
fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab =
blanchet@51998
  1788
  Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish)
blanchet@47946
  1789
                  sym_tab []
blanchet@42573
  1790
blanchet@43085
  1791
(***************************************************************)
blanchet@43085
  1792
(* Type Classes Present in the Axiom or Conjecture Clauses     *)
blanchet@43085
  1793
(***************************************************************)
blanchet@43085
  1794
blanchet@43085
  1795
fun set_insert (x, s) = Symtab.update (x, ()) s
blanchet@43085
  1796
blanchet@48142
  1797
fun add_classes (cls, cset) = List.foldl set_insert cset (flat cls)
blanchet@43085
  1798
blanchet@43093
  1799
fun classes_of_terms get_Ts =
blanchet@43121
  1800
  map (map snd o get_Ts)
blanchet@48142
  1801
  #> List.foldl add_classes Symtab.empty #> Symtab.delete_safe class_of_types
blanchet@48142
  1802
  #> Symtab.keys
blanchet@43085
  1803
wenzelm@44121
  1804
val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
wenzelm@44121
  1805
val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
blanchet@43085
  1806
blanchet@52026
  1807
fun fold_type_ctrs f (Type (s, Ts)) x = fold (fold_type_ctrs f) Ts (f (s, x))
blanchet@52026
  1808
  | fold_type_ctrs _ _ x = x
blanchet@43085
  1809
blanchet@43907
  1810
(* Type constructors used to instantiate overloaded constants are the only ones
blanchet@43907
  1811
   needed. *)
blanchet@52026
  1812
fun add_type_ctrs_in_term thy =
blanchet@43085
  1813
  let
blanchet@43188
  1814
    fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
blanchet@43181
  1815
      | add (t $ u) = add t #> add u
blanchet@44738
  1816
      | add (Const x) =
blanchet@52026
  1817
        x |> robust_const_type_args thy |> fold (fold_type_ctrs set_insert)
blanchet@43181
  1818
      | add (Abs (_, _, u)) = add u
blanchet@43181
  1819
      | add _ = I
blanchet@43181
  1820
  in add end
blanchet@43085
  1821
blanchet@52026
  1822
fun type_ctrs_of_terms thy ts =
blanchet@52026
  1823
  Symtab.keys (fold (add_type_ctrs_in_term thy) ts Symtab.empty)
blanchet@43085
  1824
blanchet@45511
  1825
fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
blanchet@45511
  1826
    let val (head, args) = strip_comb t in
blanchet@45511
  1827
      (head |> dest_Const |> fst,
blanchet@45511
  1828
       fold_rev (fn t as Var ((s, _), T) =>
blanchet@45511
  1829
                    (fn u => Abs (s, T, abstract_over (t, u)))
blanchet@47932
  1830
                  | _ => raise Fail "expected \"Var\"") args u)
blanchet@45511
  1831
    end
blanchet@45511
  1832
  | extract_lambda_def _ = raise Fail "malformed lifted lambda"
blanchet@45508
  1833
blanchet@52031
  1834
fun trans_lams_of_string ctxt type_enc lam_trans =
blanchet@45514
  1835
  if lam_trans = no_lamsN then
blanchet@45514
  1836
    rpair []
blanchet@45514
  1837
  else if lam_trans = hide_lamsN then
blanchet@45514
  1838
    lift_lams ctxt type_enc ##> K []
blanchet@46365
  1839
  else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
blanchet@45514
  1840
    lift_lams ctxt type_enc
blanchet@46365
  1841
  else if lam_trans = combsN then
blanchet@45514
  1842
    map (introduce_combinators ctxt) #> rpair []
blanchet@46365
  1843
  else if lam_trans = combs_and_liftingN then
blanchet@46365
  1844
    lift_lams_part_1 ctxt type_enc
blanchet@46365
  1845
    ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
blanchet@46818
  1846
    #> lift_lams_part_2 ctxt
blanchet@46368
  1847
  else if lam_trans = combs_or_liftingN then
blanchet@45554
  1848
    lift_lams_part_1 ctxt type_enc
blanchet@54829
  1849
    ##> map (fn t => (case head_of (strip_qnt_body @{const_name All} t) of
blanchet@46368
  1850
                       @{term "op =::bool => bool => bool"} => t
blanchet@54829
  1851
                     | _ => introduce_combinators ctxt (intentionalize_def t)))
blanchet@46818
  1852
    #> lift_lams_part_2 ctxt
blanchet@45514
  1853
  else if lam_trans = keep_lamsN then
blanchet@45514
  1854
    map (Envir.eta_contract) #> rpair []
blanchet@45514
  1855
  else
blanchet@45519
  1856
    error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
blanchet@45514
  1857
blanchet@47981
  1858
val pull_and_reorder_definitions =
blanchet@47975
  1859
  let
blanchet@47975
  1860
    fun add_consts (IApp (t, u)) = fold add_consts [t, u]
blanchet@47975
  1861
      | add_consts (IAbs (_, t)) = add_consts t
blanchet@47975
  1862
      | add_consts (IConst (name, _, _)) = insert (op =) name
blanchet@47975
  1863
      | add_consts (IVar _) = I
blanchet@47981
  1864
    fun consts_of_hs l_or_r ({iformula, ...} : ifact) =
blanchet@54829
  1865
      (case iformula of
blanchet@47975
  1866
        AAtom (IApp (IApp (IConst _, t), u)) => add_consts (l_or_r (t, u)) []
blanchet@54829
  1867
      | _ => [])
blanchet@47975
  1868
    (* Quadratic, but usually OK. *)
blanchet@47981
  1869
    fun reorder [] [] = []
blanchet@47981
  1870
      | reorder (fact :: skipped) [] =
blanchet@47981
  1871
        fact :: reorder [] skipped (* break cycle *)
blanchet@47981
  1872
      | reorder skipped (fact :: facts) =
blanchet@47975
  1873
        let val rhs_consts = consts_of_hs snd fact in
blanchet@48096
  1874
          if exists (exists (exists (member (op =) rhs_consts)
blanchet@48096
  1875
                     o consts_of_hs fst)) [skipped, facts] then
blanchet@47981
  1876
            reorder (fact :: skipped) facts
blanchet@47975
  1877
          else
blanchet@47981
  1878
            fact :: reorder [] (facts @ skipped)
blanchet@47975
  1879
        end
blanchet@47981
  1880
  in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
blanchet@47975
  1881
blanchet@54768
  1882
fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
wenzelm@56245
  1883
  | s_not_prop (@{const Pure.imp} $ t $ @{prop False}) = t
wenzelm@56245
  1884
  | s_not_prop t = @{const Pure.imp} $ t $ @{prop False}
blanchet@54768
  1885
blanchet@47975
  1886
fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
blanchet@45514
  1887
                       concl_t facts =
blanchet@42573
  1888
  let
blanchet@42573
  1889
    val thy = Proof_Context.theory_of ctxt
blanchet@52031
  1890
    val trans_lams = trans_lams_of_string ctxt type_enc lam_trans
blanchet@43861
  1891
    val fact_ts = facts |> map snd
blanchet@54829
  1892
    (* Remove existing facts from the conjecture, as this can dramatically boost an ATP's
blanchet@54829
  1893
       performance (for some reason). *)
blanchet@54829
  1894
    val hyp_ts = hyp_ts |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
blanchet@43864
  1895
    val facts = facts |> map (apsnd (pair Axiom))
blanchet@43864
  1896
    val conjs =
blanchet@47975
  1897
      map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
blanchet@45168
  1898
      |> map (apsnd freeze_term)
blanchet@54829
  1899
      |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts)
blanchet@45554
  1900
    val ((conjs, facts), lam_facts) =
blanchet@45511
  1901
      (conjs, facts)
blanchet@47769
  1902
      |> presimp ? pairself (map (apsnd (apsnd (presimp_prop ctxt type_enc))))
blanchet@45514
  1903
      |> (if lam_trans = no_lamsN then
blanchet@45511
  1904
            rpair []
blanchet@45511
  1905
          else
blanchet@45511
  1906
            op @
blanchet@45514
  1907
            #> preprocess_abstractions_in_terms trans_lams
blanchet@45511
  1908
            #>> chop (length conjs))
blanchet@47981
  1909
    val conjs =
blanchet@47981
  1910
      conjs |> make_conjecture ctxt format type_enc
blanchet@47981
  1911
            |> pull_and_reorder_definitions
blanchet@47981
  1912
    val facts =
blanchet@47981
  1913
      facts |> map_filter (fn (name, (_, t)) =>
blanchet@47981
  1914
                              make_fact ctxt format type_enc true (name, t))
blanchet@47981
  1915
            |> pull_and_reorder_definitions
blanchet@54829
  1916
    val fact_names = facts |> map (fn {name, stature, ...} : ifact => (name, stature))
blanchet@46375
  1917
    val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
blanchet@54829
  1918
    val lam_facts = lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
blanchet@43861
  1919
    val all_ts = concl_t :: hyp_ts @ fact_ts
blanchet@42573
  1920
    val subs = tfree_classes_of_terms all_ts
blanchet@42573
  1921
    val supers = tvar_classes_of_terms all_ts
blanchet@52026
  1922
    val tycons = type_ctrs_of_terms thy all_ts
blanchet@48142
  1923
    val (supers, tcon_clauses) =
blanchet@43626
  1924
      if level_of_type_enc type_enc = No_Types then ([], [])
blanchet@48142
  1925
      else make_tcon_clauses thy tycons supers
blanchet@48142
  1926
    val subclass_pairs = make_subclass_pairs thy subs supers
blanchet@42573
  1927
  in
blanchet@45508
  1928
    (fact_names |> map single, union (op =) subs supers, conjs,
blanchet@48142
  1929
     facts @ lam_facts, subclass_pairs, tcon_clauses, lifted)
blanchet@42573
  1930
  end
blanchet@42573
  1931
nik@44495
  1932
val type_guard = `(make_fixed_const NONE) type_guard_name
blanchet@43130
  1933
blanchet@47768
  1934
fun type_guard_iterm type_enc T tm =
blanchet@44396
  1935
  IApp (IConst (type_guard, T --> @{typ bool}, [T])
blanchet@47768
  1936
        |> mangle_type_args_in_iterm type_enc, tm)
blanchet@42573
  1937
blanchet@43421
  1938
fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
blanchet@48132
  1939
  | is_var_positively_naked_in_term name _ (ATerm (((s, _), _), tms)) accum =
blanchet@54829
  1940
    accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm ((name, []), [])))
blanchet@43692
  1941
  | is_var_positively_naked_in_term _ _ _ _ = true
blanchet@44403
  1942
blanchet@48186
  1943
fun is_var_undercover_in_term thy name pos tm accum =
blanchet@48186
  1944
  accum orelse
blanchet@44811
  1945
  let
blanchet@48132
  1946
    val var = ATerm ((name, []), [])
blanchet@48095
  1947
    fun is_undercover (ATerm (_, [])) = false
blanchet@48132
  1948
      | is_undercover (ATerm (((s, _), _), tms)) =
blanchet@45948
  1949
        let
blanchet@45948
  1950
          val ary = length tms
blanchet@48200
  1951
          val cover = type_arg_cover thy pos s ary
blanchet@45948
  1952
        in
blanchet@48087
  1953
          exists (fn (j, tm) => tm = var andalso member (op =) cover j)
blanchet@48087
  1954
                 (0 upto ary - 1 ~~ tms) orelse
blanchet@48095
  1955
          exists is_undercover tms
blanchet@45948
  1956
        end
blanchet@48095
  1957
      | is_undercover _ = true
blanchet@48095
  1958
  in is_undercover tm end
blanchet@44811
  1959
blanchet@48087
  1960
fun should_guard_var_in_formula thy level pos phi (SOME true) name =
blanchet@48183
  1961
    (case level of
blanchet@54829
  1962
      All_Types => true
blanchet@54829
  1963
    | Undercover_Types => formula_fold pos (is_var_undercover_in_term thy name) phi false
blanchet@54829
  1964
    | Nonmono_Types (_, Uniform) => true
blanchet@54829
  1965
    | Nonmono_Types (_, Non_Uniform) =>
blanchet@54829
  1966
      formula_fold pos (is_var_positively_naked_in_term name) phi false
blanchet@54829
  1967
    | _ => false)
blanchet@48087
  1968
  | should_guard_var_in_formula _ _ _ _ _ _ = true
blanchet@45948
  1969
blanchet@48087
  1970
fun always_guard_var_in_formula _ _ _ _ _ _ = true
blanchet@42834
  1971
blanchet@44405
  1972
fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
blanchet@44768
  1973
  | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
blanchet@48183
  1974
    not (is_type_level_uniform level) andalso
blanchet@44782
  1975
    should_encode_type ctxt mono level T
blanchet@44405
  1976
  | should_generate_tag_bound_decl _ _ _ _ _ = false
blanchet@44404
  1977
blanchet@47768
  1978
fun mk_aterm type_enc name T_args args =
blanchet@48133
  1979
  let val (ty_args, tm_args) = process_type_args type_enc T_args in
blanchet@48133
  1980
    ATerm ((name, ty_args), tm_args @ args)
blanchet@48133
  1981
  end
blanchet@42994
  1982
blanchet@47768
  1983
fun do_bound_type ctxt mono type_enc =
blanchet@54820
  1984
  (case type_enc of
blanchet@47767
  1985
    Native (_, _, level) =>
blanchet@54820
  1986
    fused_type ctxt mono level 0 #> native_atp_type_of_typ type_enc false 0 #> SOME
blanchet@54820
  1987
  | _ => K NONE)
blanchet@46392
  1988
blanchet@47768
  1989
fun tag_with_type ctxt mono type_enc pos T tm =
blanchet@43859
  1990
  IConst (type_tag, T --> T, [T])
blanchet@47768
  1991
  |> mangle_type_args_in_iterm type_enc
blanchet@53586
  1992
  |> atp_term_of_iterm ctxt mono type_enc pos
blanchet@48132
  1993
  |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm])
blanchet@43692
  1994
       | _ => raise Fail "unexpected lambda-abstraction")
blanchet@53586
  1995
and atp_term_of_iterm ctxt mono type_enc pos =
blanchet@42573
  1996
  let
blanchet@45949
  1997
    fun term site u =
blanchet@42962
  1998
      let
blanchet@43859
  1999
        val (head, args) = strip_iterm_comb u
blanchet@54829
  2000
        val pos = (case site of Top_Level pos => pos | Eq_Arg pos => pos | _ => NONE)
blanchet@48200
  2001
        val T = ityp_of u
nik@43677
  2002
        val t =
blanchet@54829
  2003
          (case head of
blanchet@43859
  2004
            IConst (name as (s, _), _, T_args) =>
blanchet@47153
  2005
            let
blanchet@48146
  2006
              val ary = length args
blanchet@54829
  2007
              fun arg_site j = if is_tptp_equal s then Eq_Arg pos else Arg (s, j, ary)
blanchet@48146
  2008
            in
blanchet@48146
  2009
              map2 (fn j => term (arg_site j)) (0 upto ary - 1) args
blanchet@48146
  2010
              |> mk_aterm type_enc name T_args
blanchet@48146
  2011
            end
blanchet@43859
  2012
          | IVar (name, _) =>
blanchet@47768
  2013
            map (term Elsewhere) args |> mk_aterm type_enc name []
blanchet@43859
  2014
          | IAbs ((name, T), tm) =>
blanchet@46818
  2015
            if is_type_enc_higher_order type_enc then
blanchet@54820
  2016
              AAbs (((name, native_atp_type_of_typ type_enc true 0 T), (* FIXME? why "true"? *)
blanchet@47911
  2017
                     term Elsewhere tm), map (term Elsewhere) args)
blanchet@46818
  2018
            else
blanchet@46818
  2019
              raise Fail "unexpected lambda-abstraction"
blanchet@54829
  2020
          | IApp _ => raise Fail "impossible \"IApp\"")
blanchet@48200
  2021
        val tag = should_tag_with_type ctxt mono type_enc site u T
blanchet@48200
  2022
      in t |> tag ? tag_with_type ctxt mono type_enc pos T end
blanchet@47911
  2023
  in term (Top_Level pos) end
blanchet@52031
  2024
and formula_of_iformula ctxt mono type_enc should_guard_var =
blanchet@42829
  2025
  let
blanchet@44811
  2026
    val thy = Proof_Context.theory_of ctxt
blanchet@44811
  2027
    val level = level_of_type_enc type_enc
blanchet@53586
  2028
    val do_term = atp_term_of_iterm ctxt mono type_enc
blanchet@42878
  2029
    fun do_out_of_bound_type pos phi universal (name, T) =
blanchet@44399
  2030
      if should_guard_type ctxt mono type_enc
blanchet@48087
  2031
             (fn () => should_guard_var thy level pos phi universal name) T then
blanchet@43859
  2032
        IVar (name, T)
blanchet@47768
  2033
        |> type_guard_iterm type_enc T
blanchet@43361
  2034
        |> do_term pos |> AAtom |> SOME
blanchet@44405
  2035
      else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
blanchet@44405
  2036
        let
blanchet@48132
  2037
          val var = ATerm ((name, []), [])
blanchet@47768
  2038
          val tagged_var = tag_with_type ctxt mono type_enc pos T var
blanchet@48132
  2039
        in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end
blanchet@42573
  2040
      else
blanchet@42573
  2041
        NONE
blanchet@48133
  2042
    fun do_formula pos (ATyQuant (q, xs, phi)) =
blanchet@54820
  2043
        ATyQuant (q, map (apfst (native_atp_type_of_typ type_enc false 0)) xs, do_formula pos phi)
blanchet@48133
  2044
      | do_formula pos (AQuant (q, xs, phi)) =
blanchet@42878
  2045
        let
blanchet@42878
  2046
          val phi = phi |> do_formula pos
blanchet@42878
  2047
          val universal = Option.map (q = AExists ? not) pos
blanchet@47768
  2048
          val do_bound_type = do_bound_type ctxt mono type_enc
blanchet@42878
  2049
        in
blanchet@42834
  2050
          AQuant (q, xs |> map (apsnd (fn NONE => NONE
blanchet@42834
  2051
                                        | SOME T => do_bound_type T)),
blanchet@42834
  2052
                  (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
blanchet@42834
  2053
                      (map_filter
blanchet@42834
  2054
                           (fn (_, NONE) => NONE
blanchet@42834
  2055
                             | (s, SOME T) =>
blanchet@42878
  2056
                               do_out_of_bound_type pos phi universal (s, T))
blanchet@42878
  2057
                           xs)
blanchet@42834
  2058
                      phi)
blanchet@42834
  2059
        end
blanchet@42878
  2060
      | do_formula pos (AConn conn) = aconn_map pos do_formula conn
blanchet@43361
  2061
      | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
blanchet@43493
  2062
  in do_formula end
blanchet@42573
  2063
blanchet@48438
  2064
fun string_of_status General = ""
blanchet@48438
  2065
  | string_of_status Induction = inductionN
blanchet@48438
  2066
  | string_of_status Intro = introN
blanchet@48438
  2067
  | string_of_status Inductive = inductiveN
blanchet@48438
  2068
  | string_of_status Elim = elimN
blanchet@48438
  2069
  | string_of_status Simp = simpN
blanchet@48438
  2070
  | string_of_status Non_Rec_Def = non_rec_defN
blanchet@48438
  2071
  | string_of_status Rec_Def = rec_defN
blanchet@48438
  2072
blanchet@42573
  2073
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
blanchet@52032
  2074
   of monomorphization). The TPTP forbids name clashes, and some of the remote
blanchet@52032
  2075
   provers might care. *)
blanchet@51998
  2076
fun line_of_fact ctxt prefix encode alt freshen pos mono type_enc rank
blanchet@48438
  2077
        (j, {name, stature = (_, status), role, iformula, atomic_types}) =
blanchet@50521
  2078
  Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
blanchet@50758
  2079
            encode name, alt name),
blanchet@48438
  2080
           role,
blanchet@48438
  2081
           iformula
blanchet@52031
  2082
           |> formula_of_iformula ctxt mono type_enc
blanchet@48438
  2083
                  should_guard_var_in_formula (if pos then SOME true else NONE)
blanchet@48438
  2084
           |> close_formula_universally
blanchet@48438
  2085
           |> bound_tvars type_enc true atomic_types,
blanchet@48438
  2086
           NONE, isabelle_info (string_of_status status) (rank j))
blanchet@42573
  2087
blanchet@51998
  2088
fun lines_of_subclass type_enc sub super =
blanchet@50521
  2089
  Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
blanchet@48133
  2090
           AConn (AImplies,
blanchet@48142
  2091
                  [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
blanchet@48133
  2092
           |> bound_tvars type_enc false [tvar_a],
blanchet@48133
  2093
           NONE, isabelle_info inductiveN helper_rank)
blanchet@48133
  2094
blanchet@51998
  2095
fun lines_of_subclass_pair type_enc (sub, supers) =
blanchet@48142
  2096
  if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
blanchet@48142
  2097
    [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub,
blanchet@48142
  2098
                 map (`make_class) supers)]
blanchet@48142
  2099
  else
blanchet@51998
  2100
    map (lines_of_subclass type_enc sub) supers
blanchet@48142
  2101
blanchet@51998
  2102
fun line_of_tcon_clause type_enc (name, prems, (cl, T)) =
blanchet@48142
  2103
  if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
blanchet@48142
  2104
    Class_Memb (class_memb_prefix ^ name,
blanchet@54820
  2105
      map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems,
blanchet@54820
  2106
      native_atp_type_of_typ type_enc false 0 T, `make_class cl)
blanchet@48142
  2107
  else
blanchet@50521
  2108
    Formula ((tcon_clause_prefix ^ name, ""), Axiom,
blanchet@48142
  2109
             mk_ahorn (maps (class_atoms type_enc) prems)
blanchet@48142
  2110
                      (class_atom type_enc (cl, T))
blanchet@48142
  2111
             |> bound_tvars type_enc true (snd (dest_Type T)),
blanchet@47148
  2112
             NONE, isabelle_info inductiveN helper_rank)
blanchet@42573
  2113
blanchet@51998
  2114
fun line_of_conjecture ctxt mono type_enc
blanchet@51998
  2115
                       ({name, role, iformula, atomic_types, ...} : ifact) =
blanchet@50521
  2116
  Formula ((conjecture_prefix ^ name, ""), role,
blanchet@45316
  2117
           iformula
blanchet@52031
  2118
           |> formula_of_iformula ctxt mono type_enc
blanchet@45316
  2119
                  should_guard_var_in_formula (SOME false)
blanchet@45377
  2120
           |> close_formula_universally
blanchet@46406
  2121
           |> bound_tvars type_enc true atomic_types, NONE, [])
blanchet@42573
  2122
blanchet@51998
  2123
fun lines_of_free_types type_enc (facts : ifact list) =
blanchet@48185
  2124
  if is_type_enc_polymorphic type_enc then
blanchet@48185
  2125
    let
blanchet@54798
  2126
      val type_classes = (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic)
blanchet@48185
  2127
      fun line j (cl, T) =
blanchet@48185
  2128
        if type_classes then
blanchet@48185
  2129
          Class_Memb (class_memb_prefix ^ string_of_int j, [],
blanchet@54820
  2130
            native_atp_type_of_typ type_enc false 0 T, `make_class cl)
blanchet@48185
  2131
        else
blanchet@50521
  2132
          Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis,
blanchet@54820
  2133
            class_atom type_enc (cl, T), NONE, [])
blanchet@48185
  2134
      val membs =
blanchet@48185
  2135
        fold (union (op =)) (map #atomic_types facts) []
blanchet@51998
  2136
        |> class_membs_of_types type_enc add_sorts_on_tfree
blanchet@54798
  2137
    in
blanchet@54798
  2138
      map2 line (0 upto length membs - 1) membs
blanchet@54798
  2139
    end
blanchet@48185
  2140
  else
blanchet@48185
  2141
    []
blanchet@42573
  2142
blanchet@42573
  2143
(** Symbol declarations **)
blanchet@42544
  2144
blanchet@51998
  2145
fun decl_line_of_class phantoms s =
blanchet@48142
  2146
  let val name as (s, _) = `make_class s in
blanchet@48137
  2147
    Sym_Decl (sym_decl_prefix ^ s, name,
blanchet@48137
  2148
              APi ([tvar_a_name],
blanchet@48137
  2149
                   if phantoms = Without_Phantom_Type_Vars then
blanchet@48137
  2150
                     AFun (a_itself_atype, bool_atype)
blanchet@48137
  2151
                   else
blanchet@48137
  2152
                     bool_atype))
blanchet@44595
  2153
  end
blanchet@44595
  2154
blanchet@51998
  2155
fun decl_lines_of_classes type_enc =
blanchet@54829
  2156
  (case type_enc of
blanchet@54829
  2157
    Native (_, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms)
blanchet@54829
  2158
  | _ => K [])
blanchet@44595
  2159
blanchet@51998
  2160
fun sym_decl_table_of_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
blanchet@42574
  2161
  let
blanchet@44829
  2162
    fun add_iterm_syms tm =
blanchet@43859
  2163
      let val (head, args) = strip_iterm_comb tm in
blanchet@42574
  2164
        (case head of
blanchet@54829
  2165
          IConst ((s, s'), T, T_args) =>
blanchet@54829
  2166
          let
blanchet@54829
  2167
            val (pred_sym, in_conj) =
blanchet@54829
  2168
              (case Symtab.lookup sym_tab s of
blanchet@54829
  2169
                SOME ({pred_sym, in_conj, ...} : sym_info) => (pred_sym, in_conj)
blanchet@54829
  2170
              | NONE => (false, false))
blanchet@54829
  2171
            val decl_sym =
blanchet@54829
  2172
              (case type_enc of Guards _ => not pred_sym | _ => true) andalso is_tptp_user_symbol s
blanchet@54829
  2173
          in
blanchet@54829
  2174
            if decl_sym then
blanchet@54829
  2175
              Symtab.map_default (s, [])
blanchet@54829
  2176
                (insert_type thy #3 (s', T_args, T, pred_sym, length args, in_conj))
blanchet@54829
  2177
            else
blanchet@54829
  2178
              I
blanchet@54829
  2179
          end
blanchet@54829
  2180
        | IAbs (_, tm) => add_iterm_syms tm
blanchet@54829
  2181
        | _ => I)
blanchet@44829
  2182
        #> fold add_iterm_syms args
blanchet@42574
  2183
      end
blanchet@50968
  2184
    val add_fact_syms = ifact_lift (formula_fold NONE (K add_iterm_syms))
blanchet@48133
  2185
    fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi
blanchet@48133
  2186
      | add_formula_var_types (AQuant (_, xs, phi)) =
blanchet@47150
  2187
        fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
blanchet@43966
  2188
        #> add_formula_var_types phi
blanchet@43966
  2189
      | add_formula_var_types (AConn (_, phis)) =
blanchet@43966
  2190
        fold add_formula_var_types phis
blanchet@43966
  2191
      | add_formula_var_types _ = I
blanchet@43966
  2192
    fun var_types () =
blanchet@48131
  2193
      if is_type_enc_polymorphic type_enc then [tvar_a]
blanchet@47981
  2194
      else fold (ifact_lift add_formula_var_types) (conjs @ facts) []
blanchet@43966
  2195
    fun add_undefined_const T =
blanchet@43984
  2196
      let
blanchet@48200
  2197
        (* FIXME: make sure type arguments are filtered / clean up code *)
blanchet@43984
  2198
        val (s, s') =
blanchet@44622
  2199
          `(make_fixed_const NONE) @{const_name undefined}
blanchet@48201
  2200
          |> (is_type_enc_mangling type_enc ? mangled_const_name type_enc [T])
blanchet@43984
  2201
      in
blanchet@43984
  2202
        Symtab.map_default (s, [])
blanchet@47150
  2203
                           (insert_type thy #3 (s', [T], T, false, 0, false))
blanchet@43984
  2204
      end
blanchet@44622
  2205
    fun add_TYPE_const () =
blanchet@44622
  2206
      let val (s, s') = TYPE_name in
blanchet@44622
  2207
        Symtab.map_default (s, [])
blanchet@47150
  2208
            (insert_type thy #3
blanchet@44622
  2209
                         (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
blanchet@44622
  2210
      end
blanchet@42698
  2211
  in
blanchet@42698
  2212
    Symtab.empty
blanchet@48089
  2213
    |> is_type_enc_sound type_enc
blanchet@44829
  2214
       ? (fold (fold add_fact_syms) [conjs, facts]
blanchet@46392
  2215
          #> fold add_iterm_syms extra_tms
blanchet@43985
  2216
          #> (case type_enc of
blanchet@48131
  2217
                Native (First_Order, Raw_Polymorphic phantoms, _) =>
blanchet@48131
  2218
                phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
blanchet@47767
  2219
              | Native _ => I
blanchet@43985
  2220
              | _ => fold add_undefined_const (var_types ())))
blanchet@42698
  2221
  end
blanchet@42533
  2222
blanchet@44399
  2223
(* We add "bool" in case the helper "True_or_False" is included later. *)
blanchet@48143
  2224
fun default_mono level completish =
blanchet@44399
  2225
  {maybe_finite_Ts = [@{typ bool}],
blanchet@54829
  2226
   surely_infinite_Ts = (case level of Nonmono_Types (Strict, _) => [] | _ => known_infinite_types),
blanchet@48143
  2227
   maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]}
blanchet@44399
  2228
blanchet@50968
  2229
(* This inference is described in section 4 of Blanchette et al., "Encoding
blanchet@50968
  2230
   monomorphic and polymorphic types", TACAS 2013. *)
blanchet@44399
  2231
fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
blanchet@44399
  2232
  | add_iterm_mononotonicity_info ctxt level _
blanchet@44399
  2233
        (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
blanchet@48103
  2234
        (mono as {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}) =
blanchet@47150
  2235
    let val thy = Proof_Context.theory_of ctxt in
blanchet@47150
  2236
      if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
blanchet@54829
  2237
        (case level of
blanchet@48092
  2238
          Nonmono_Types (strictness, _) =>
blanchet@47150
  2239
          if exists (type_instance thy T) surely_infinite_Ts orelse
blanchet@47150
  2240
             member (type_equiv thy) maybe_finite_Ts T then
blanchet@47150
  2241
            mono
blanchet@47150
  2242
          else if is_type_kind_of_surely_infinite ctxt strictness
blanchet@47150
  2243
                                                  surely_infinite_Ts T then
blanchet@47150
  2244
            {maybe_finite_Ts = maybe_finite_Ts,
blanchet@47150
  2245
             surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
blanchet@47150
  2246
             maybe_nonmono_Ts = maybe_nonmono_Ts}
blanchet@47150
  2247
          else
blanchet@47150
  2248
            {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
blanchet@47150
  2249
             surely_infinite_Ts = surely_infinite_Ts,
blanchet@47150
  2250
             maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
blanchet@54829
  2251
        | _ => mono)
blanchet@47150
  2252
      else
blanchet@47150
  2253
        mono
blanchet@47150
  2254
    end
blanchet@44399
  2255
  | add_iterm_mononotonicity_info _ _ _ _ mono = mono
blanchet@47981
  2256
fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) =
blanchet@47975
  2257
  formula_fold (SOME (role <> Conjecture))
blanchet@44399
  2258
               (add_iterm_mononotonicity_info ctxt level) iformula
blanchet@51998
  2259
fun mononotonicity_info_of_facts ctxt type_enc completish facts =
blanchet@43626
  2260
  let val level = level_of_type_enc type_enc in
blanchet@48143
  2261
    default_mono level completish
blanchet@44399
  2262
    |> is_type_level_monotonicity_based level
blanchet@44399
  2263
       ? fold (add_fact_mononotonicity_info ctxt level) facts
blanchet@42829
  2264
  end
blanchet@42677
  2265
blanchet@52005
  2266
fun fold_arg_types f (IApp (tm1, tm2)) =
blanchet@52005
  2267
    fold_arg_types f tm1 #> fold_term_types f tm2
blanchet@52005
  2268
  | fold_arg_types _ _ = I
blanchet@52005
  2269
and fold_term_types f tm = f (ityp_of tm) #> fold_arg_types f tm
blanchet@52005
  2270
blanchet@44501
  2271
fun add_iformula_monotonic_types ctxt mono type_enc =
blanchet@44501
  2272
  let
blanchet@47150
  2273
    val thy = Proof_Context.theory_of ctxt
blanchet@44501
  2274
    val level = level_of_type_enc type_enc
blanchet@44501
  2275
    val should_encode = should_encode_type ctxt mono level
blanchet@47150
  2276
    fun add_type T = not (should_encode T) ? insert_type thy I T
blanchet@52005
  2277
  in formula_fold NONE (K (fold_term_types add_type)) end
blanchet@50968
  2278
blanchet@44501
  2279
fun add_fact_monotonic_types ctxt mono type_enc =
blanchet@50968
  2280
  ifact_lift (add_iformula_monotonic_types ctxt mono type_enc)
blanchet@50968
  2281
blanchet@51998
  2282
fun monotonic_types_of_facts ctxt mono type_enc facts =
blanchet@44811
  2283
  let val level = level_of_type_enc type_enc in
blanchet@48131
  2284
    [] |> (is_type_enc_polymorphic type_enc andalso
blanchet@48183
  2285
           is_type_level_monotonicity_based level)
blanchet@44811
  2286
          ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
blanchet@44811
  2287
  end
blanchet@44501
  2288
blanchet@51998
  2289
fun line_of_guards_mono_type ctxt mono type_enc T =
blanchet@50521
  2290
  Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
blanchet@44396
  2291
           Axiom,
blanchet@44396
  2292
           IConst (`make_bound_var "X", T, [])
blanchet@47768
  2293
           |> type_guard_iterm type_enc T
blanchet@44396
  2294
           |> AAtom
blanchet@52031
  2295
           |> formula_of_iformula ctxt mono type_enc always_guard_var_in_formula
blanchet@52031
  2296
                                  (SOME true)
blanchet@45377
  2297
           |> close_formula_universally
blanchet@45920
  2298
           |> bound_tvars type_enc true (atomic_types_of T),
blanchet@47148
  2299
           NONE, isabelle_info inductiveN helper_rank)
blanchet@44396
  2300
blanchet@51998
  2301
fun line_of_tags_mono_type ctxt mono type_enc T =
blanchet@48132
  2302
  let val x_var = ATerm ((`make_bound_var "X", []), []) in
blanchet@54798
  2303
    Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom,
blanchet@46392
  2304
             eq_formula type_enc (atomic_types_of T) [] false
blanchet@47768
  2305
                  (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
blanchet@48438
  2306
             NONE, isabelle_info non_rec_defN helper_rank)
blanchet@44396
  2307
  end
blanchet@44396
  2308
blanchet@51998
  2309
fun lines_of_mono_types ctxt mono type_enc =
blanchet@54829
  2310
  (case type_enc of
blanchet@51998
  2311
    Native _ => K []
blanchet@51998
  2312
  | Guards _ => map (line_of_guards_mono_type ctxt mono type_enc)
blanchet@54829
  2313
  | Tags _ => map (line_of_tags_mono_type ctxt mono type_enc))
blanchet@44396
  2314
blanchet@51998
  2315
fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) =
blanchet@42994
  2316
  let
blanchet@44594
  2317
    val thy = Proof_Context.theory_of ctxt
blanchet@44594
  2318
    val (T, T_args) =
blanchet@44594
  2319
      if null T_args then
blanchet@44594
  2320
        (T, [])
blanchet@54829
  2321
      else
blanchet@54829
  2322
        (case unprefix_and_unascii const_prefix s of
blanchet@54829
  2323
          SOME s' =>
blanchet@54829
  2324
          let
blanchet@54829
  2325
            val s' = s' |> unmangled_invert_const
blanchet@54829
  2326
            val T = s' |> robust_const_type thy
blanchet@54829
  2327
          in (T, robust_const_type_args thy (s', T)) end
blanchet@54829
  2328
        | NONE => raise Fail "unexpected type arguments")
blanchet@42994
  2329
  in
blanchet@48137
  2330
    Sym_Decl (sym_decl_prefix ^ s, (s, s'),
blanchet@48137
  2331
              T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
blanchet@54820
  2332
                |> native_atp_type_of_typ type_enc pred_sym ary
blanchet@48137
  2333
                |> not (null T_args)
blanchet@48142
  2334
                   ? curry APi (map (tvar_name o dest_TVar) T_args))
blanchet@42994
  2335
  end
blanchet@42579
  2336
blanchet@50968
  2337
fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
blanchet@46392
  2338
blanchet@51998
  2339
fun line_of_guards_sym_decl ctxt mono type_enc n s