src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
author blanchet
Mon, 30 May 2011 17:00:38 +0200
changeset 43064 b6e61d22fa61
parent 43039 b967219cec78
permissions -rw-r--r--
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40114
blanchet
parents: 40069
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
     3
    Author:     Makarius
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
     5
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39452
diff changeset
     6
Translation of HOL to FOL for Sledgehammer.
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
     7
*)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
     8
40068
ed2869dd9bfa renamed modules
blanchet
parents: 40067
diff changeset
     9
signature SLEDGEHAMMER_ATP_TRANSLATE =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    10
sig
42227
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 42180
diff changeset
    11
  type 'a fo_term = 'a ATP_Problem.fo_term
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42895
diff changeset
    12
  type format = ATP_Problem.format
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
    13
  type formula_kind = ATP_Problem.formula_kind
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    14
  type 'a problem = 'a ATP_Problem.problem
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    15
  type locality = Sledgehammer_Filter.locality
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    16
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    17
  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    18
  datatype type_level =
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    19
    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    20
  datatype type_heaviness = Heavy | Light
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    21
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    22
  datatype type_system =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
    23
    Simple_Types of type_level |
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    24
    Preds of polymorphism * type_level * type_heaviness |
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    25
    Tags of polymorphism * type_level * type_heaviness
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    26
40114
blanchet
parents: 40069
diff changeset
    27
  type translated_formula
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    28
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
    29
  val readable_names : bool Config.T
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40145
diff changeset
    30
  val fact_prefix : string
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    31
  val conjecture_prefix : string
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    32
  val helper_prefix : string
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    33
  val typed_helper_suffix : string
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    34
  val predicator_name : string
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    35
  val app_op_name : string
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    36
  val type_pred_name : string
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
    37
  val simple_type_prefix : string
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    38
  val type_sys_from_string : string -> type_system
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    39
  val polymorphism_of_type_sys : type_system -> polymorphism
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    40
  val level_of_type_sys : type_system -> type_level
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    41
  val is_type_sys_virtually_sound : type_system -> bool
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    42
  val is_type_sys_fairly_sound : type_system -> bool
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
    43
  val unmangled_const : string -> string * string fo_term list
41088
54eb8e7c7f9b clarified terminology
blanchet
parents: 40204
diff changeset
    44
  val translate_atp_fact :
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
    45
    Proof.context -> format -> type_system -> bool -> (string * locality) * thm
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    46
    -> translated_formula option * ((string * locality) * thm)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39975
diff changeset
    47
  val prepare_atp_problem :
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42895
diff changeset
    48
    Proof.context -> format -> formula_kind -> formula_kind -> type_system
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
    49
    -> bool option -> term list -> term
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
    50
    -> (translated_formula option * ((string * 'a) * thm)) list
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
    51
    -> string problem * string Symtab.table * int * int
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    52
       * (string * 'a) list vector * int list * int Symtab.table
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
    53
  val atp_problem_weights : string problem -> (string * real) list
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    54
end;
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    55
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
    56
structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    57
struct
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    58
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    59
open ATP_Problem
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39452
diff changeset
    60
open Metis_Translate
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    61
open Sledgehammer_Util
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    62
open Sledgehammer_Filter
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    63
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    64
(* experimental *)
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    65
val generate_useful_info = false
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    66
42879
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    67
fun useful_isabelle_info s =
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    68
  if generate_useful_info then
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    69
    SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    70
  else
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    71
    NONE
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    72
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    73
val intro_info = useful_isabelle_info "intro"
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    74
val elim_info = useful_isabelle_info "elim"
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    75
val simp_info = useful_isabelle_info "simp"
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
    76
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    77
(* Readable names are often much shorter, especially if types are mangled in
42589
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
    78
   names. Also, the logic for generating legal SNARK sort names is only
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
    79
   implemented for readable names. Finally, readable names are, well, more
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
    80
   readable. For these reason, they are enabled by default. *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
    81
val readable_names =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
    82
  Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    83
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
    84
val type_decl_prefix = "ty_"
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
    85
val sym_decl_prefix = "sy_"
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
    86
val sym_formula_prefix = "sym_"
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40145
diff changeset
    87
val fact_prefix = "fact_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    88
val conjecture_prefix = "conj_"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    89
val helper_prefix = "help_"
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    90
val class_rel_clause_prefix = "crel_";
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    91
val arity_clause_prefix = "arity_"
39975
7c50d5ca5c04 avoid generating several formulas with the same name ("tfrees")
blanchet
parents: 39954
diff changeset
    92
val tfree_prefix = "tfree_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    93
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    94
val typed_helper_suffix = "_T"
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    95
val untyped_helper_suffix = "_U"
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    96
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    97
val predicator_name = "hBOOL"
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    98
val app_op_name = "hAPP"
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    99
val type_pred_name = "is"
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   100
val simple_type_prefix = "ty_"
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   101
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   102
fun make_simple_type s =
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   103
  if s = tptp_bool_type orelse s = tptp_fun_type orelse
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   104
     s = tptp_individual_type then
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   105
    s
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   106
  else
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   107
    simple_type_prefix ^ ascii_of s
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   108
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   109
(* Freshness almost guaranteed! *)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   110
val sledgehammer_weak_prefix = "Sledgehammer:"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   111
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   112
datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   113
datatype type_level =
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   114
  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   115
datatype type_heaviness = Heavy | Light
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   116
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   117
datatype type_system =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   118
  Simple_Types of type_level |
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   119
  Preds of polymorphism * type_level * type_heaviness |
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   120
  Tags of polymorphism * type_level * type_heaviness
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   121
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   122
fun try_unsuffixes ss s =
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   123
  fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   124
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   125
fun type_sys_from_string s =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   126
  (case try (unprefix "poly_") s of
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   127
     SOME s => (SOME Polymorphic, s)
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   128
   | NONE =>
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   129
     case try (unprefix "mono_") s of
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   130
       SOME s => (SOME Monomorphic, s)
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   131
     | NONE =>
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   132
       case try (unprefix "mangled_") s of
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   133
         SOME s => (SOME Mangled_Monomorphic, s)
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   134
       | NONE => (NONE, s))
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   135
  ||> (fn s =>
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   136
          (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   137
          case try_unsuffixes ["?", "_query"] s of
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   138
            SOME s => (Nonmonotonic_Types, s)
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   139
          | NONE =>
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   140
            case try_unsuffixes ["!", "_bang"] s of
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   141
              SOME s => (Finite_Types, s)
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   142
            | NONE => (All_Types, s))
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   143
  ||> apsnd (fn s =>
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   144
                case try (unsuffix "_heavy") s of
42854
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   145
                  SOME s => (Heavy, s)
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   146
                | NONE => (Light, s))
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   147
  |> (fn (poly, (level, (heaviness, core))) =>
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   148
         case (core, (poly, level, heaviness)) of
42855
b48529f41888 renamed "simple_types" to "simple"
blanchet
parents: 42854
diff changeset
   149
           ("simple", (NONE, _, Light)) => Simple_Types level
42854
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   150
         | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
42851
3bb63850488b removed "poly_tags_light_bang" since highly unsound
blanchet
parents: 42837
diff changeset
   151
         | ("tags", (SOME Polymorphic, All_Types, _)) =>
42854
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   152
           Tags (Polymorphic, All_Types, heaviness)
42886
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   153
         | ("tags", (SOME Polymorphic, _, _)) =>
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   154
           (* The actual light encoding is very unsound. *)
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   155
           Tags (Polymorphic, level, Heavy)
42854
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   156
         | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   157
         | ("args", (SOME poly, All_Types (* naja *), Light)) =>
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   158
           Preds (poly, Const_Arg_Types, Light)
42854
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   159
         | ("erased", (NONE, All_Types (* naja *), Light)) =>
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   160
           Preds (Polymorphic, No_Types, Light)
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   161
         | _ => raise Same.SAME)
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   162
  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   163
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   164
fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   165
  | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   166
  | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   167
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   168
fun level_of_type_sys (Simple_Types level) = level
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   169
  | level_of_type_sys (Preds (_, level, _)) = level
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   170
  | level_of_type_sys (Tags (_, level, _)) = level
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   171
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   172
fun heaviness_of_type_sys (Simple_Types _) = Heavy
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   173
  | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   174
  | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   175
42687
blanchet
parents: 42685
diff changeset
   176
fun is_type_level_virtually_sound level =
blanchet
parents: 42685
diff changeset
   177
  level = All_Types orelse level = Nonmonotonic_Types
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   178
val is_type_sys_virtually_sound =
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   179
  is_type_level_virtually_sound o level_of_type_sys
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   180
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   181
fun is_type_level_fairly_sound level =
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   182
  is_type_level_virtually_sound level orelse level = Finite_Types
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   183
val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   184
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   185
fun is_setting_higher_order THF (Simple_Types _) = true
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   186
  | is_setting_higher_order _ _ = false
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   187
40114
blanchet
parents: 40069
diff changeset
   188
type translated_formula =
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38748
diff changeset
   189
  {name: string,
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   190
   locality: locality,
42525
7a506b0b644f distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree
blanchet
parents: 42524
diff changeset
   191
   kind: formula_kind,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   192
   combformula: (name, typ, combterm) formula,
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   193
   atomic_types: typ list}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   194
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   195
fun update_combformula f ({name, locality, kind, combformula, atomic_types}
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   196
                          : translated_formula) =
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   197
  {name = name, locality = locality, kind = kind, combformula = f combformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   198
   atomic_types = atomic_types} : translated_formula
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   199
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   200
fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   201
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   202
val type_instance = Sign.typ_instance o Proof_Context.theory_of
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   203
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   204
fun insert_type ctxt get_T x xs =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   205
  let val T = get_T x in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   206
    if exists (curry (type_instance ctxt) T o get_T) xs then xs
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   207
    else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   208
  end
42677
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   209
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   210
(* The Booleans indicate whether all type arguments should be kept. *)
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   211
datatype type_arg_policy =
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   212
  Explicit_Type_Args of bool |
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   213
  Mangled_Type_Args of bool |
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   214
  No_Type_Args
41136
30bedf58b177 implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents: 41134
diff changeset
   215
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   216
fun should_drop_arg_type_args (Simple_Types _) =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   217
    false (* since TFF doesn't support overloading *)
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   218
  | should_drop_arg_type_args type_sys =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   219
    level_of_type_sys type_sys = All_Types andalso
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   220
    heaviness_of_type_sys type_sys = Heavy
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   221
42589
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
   222
fun general_type_arg_policy type_sys =
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
   223
  if level_of_type_sys type_sys = No_Types then
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
   224
    No_Type_Args
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
   225
  else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   226
    Mangled_Type_Args (should_drop_arg_type_args type_sys)
42589
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
   227
  else
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   228
    Explicit_Type_Args (should_drop_arg_type_args type_sys)
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   229
42951
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   230
fun type_arg_policy type_sys s =
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   231
  if s = @{const_name HOL.eq} orelse
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   232
     (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
42951
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   233
    No_Type_Args
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   234
  else
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   235
    general_type_arg_policy type_sys
42227
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 42180
diff changeset
   236
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
   237
fun atp_type_literals_for_types format type_sys kind Ts =
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
   238
  if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then
42353
7797efa897a1 correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents: 42237
diff changeset
   239
    []
7797efa897a1 correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents: 42237
diff changeset
   240
  else
7797efa897a1 correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents: 42237
diff changeset
   241
    Ts |> type_literals_for_types
7797efa897a1 correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents: 42237
diff changeset
   242
       |> filter (fn TyLitVar _ => kind <> Conjecture
7797efa897a1 correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents: 42237
diff changeset
   243
                   | TyLitFree _ => kind = Conjecture)
41137
8b634031b2a5 implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents: 41136
diff changeset
   244
42534
46e690db16b8 fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents: 42533
diff changeset
   245
fun mk_aconns c phis =
46e690db16b8 fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents: 42533
diff changeset
   246
  let val (phis', phi') = split_last phis in
46e690db16b8 fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents: 42533
diff changeset
   247
    fold_rev (mk_aconn c) phis' phi'
46e690db16b8 fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents: 42533
diff changeset
   248
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   249
fun mk_ahorn [] phi = phi
42534
46e690db16b8 fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents: 42533
diff changeset
   250
  | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   251
fun mk_aquant _ [] phi = phi
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   252
  | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   253
    if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   254
  | mk_aquant q xs phi = AQuant (q, xs, phi)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   255
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   256
fun close_universally atom_vars phi =
41145
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   257
  let
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   258
    fun formula_vars bounds (AQuant (_, xs, phi)) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   259
        formula_vars (map fst xs @ bounds) phi
41145
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   260
      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   261
      | formula_vars bounds (AAtom tm) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   262
        union (op =) (atom_vars tm []
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   263
                      |> filter_out (member (op =) bounds o fst))
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   264
  in mk_aquant AForall (formula_vars [] phi []) phi end
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   265
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   266
fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   267
  | combterm_vars (CombConst _) = I
42574
blanchet
parents: 42573
diff changeset
   268
  | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   269
fun close_combformula_universally phi = close_universally combterm_vars phi
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   270
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   271
fun term_vars (ATerm (name as (s, _), tms)) =
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   272
  is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   273
fun close_formula_universally phi = close_universally term_vars phi
41145
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   274
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   275
val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   276
val homo_infinite_type = Type (homo_infinite_type_name, [])
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   277
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   278
fun fo_term_from_typ higher_order =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   279
  let
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   280
    fun term (Type (s, Ts)) =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   281
      ATerm (case (higher_order, s) of
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   282
               (true, @{type_name bool}) => `I tptp_bool_type
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   283
             | (true, @{type_name fun}) => `I tptp_fun_type
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   284
             | _ => if s = homo_infinite_type_name then `I tptp_individual_type
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   285
                    else `make_fixed_type_const s,
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   286
             map term Ts)
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   287
    | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   288
    | term (TVar ((x as (s, _)), _)) =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   289
      ATerm ((make_schematic_type_var x, s), [])
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   290
  in term end
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   291
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   292
(* This shouldn't clash with anything else. *)
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   293
val mangled_type_sep = "\000"
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   294
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   295
fun generic_mangled_type_name f (ATerm (name, [])) = f name
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   296
  | generic_mangled_type_name f (ATerm (name, tys)) =
42761
8ea9c6fa8b53 fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
blanchet
parents: 42755
diff changeset
   297
    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
8ea9c6fa8b53 fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
blanchet
parents: 42755
diff changeset
   298
    ^ ")"
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   299
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   300
val bool_atype = AType (`I tptp_bool_type)
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   301
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   302
fun ho_type_from_fo_term higher_order pred_sym ary =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   303
  let
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   304
    fun to_atype ty =
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   305
      AType ((make_simple_type (generic_mangled_type_name fst ty),
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   306
              generic_mangled_type_name snd ty))
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   307
    fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   308
    fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   309
      | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   310
    fun to_ho (ty as ATerm ((s, _), tys)) =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   311
      if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   312
  in if higher_order then to_ho else to_fo ary end
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   313
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   314
fun mangled_type higher_order pred_sym ary =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   315
  ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   316
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   317
fun mangled_const_name T_args (s, s') =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   318
  let
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   319
    val ty_args = map (fo_term_from_typ false) T_args
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   320
    fun type_suffix f g =
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   321
      fold_rev (curry (op ^) o g o prefix mangled_type_sep
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   322
                o generic_mangled_type_name f) ty_args ""
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   323
  in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   324
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   325
val parse_mangled_ident =
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   326
  Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   327
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   328
fun parse_mangled_type x =
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   329
  (parse_mangled_ident
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   330
   -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   331
                    [] >> ATerm) x
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   332
and parse_mangled_types x =
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   333
  (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   334
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   335
fun unmangled_type s =
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   336
  s |> suffix ")" |> raw_explode
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   337
    |> Scan.finite Symbol.stopper
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   338
           (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   339
                                                quote s)) parse_mangled_type))
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   340
    |> fst
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   341
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   342
val unmangled_const_name = space_explode mangled_type_sep #> hd
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   343
fun unmangled_const s =
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   344
  let val ss = space_explode mangled_type_sep s in
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   345
    (hd ss, map unmangled_type (tl ss))
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   346
  end
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   347
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   348
fun introduce_proxies format type_sys =
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   349
  let
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   350
    fun intro top_level (CombApp (tm1, tm2)) =
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   351
        CombApp (intro top_level tm1, intro false tm2)
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   352
      | intro top_level (CombConst (name as (s, _), T, T_args)) =
42570
77f94ac04f32 cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents: 42569
diff changeset
   353
        (case proxify_const s of
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   354
           SOME (_, proxy_base) =>
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   355
           if top_level orelse is_setting_higher_order format type_sys then
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   356
             case (top_level, s) of
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   357
               (_, "c_False") => (`I tptp_false, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   358
             | (_, "c_True") => (`I tptp_true, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   359
             | (false, "c_Not") => (`I tptp_not, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   360
             | (false, "c_conj") => (`I tptp_and, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   361
             | (false, "c_disj") => (`I tptp_or, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   362
             | (false, "c_implies") => (`I tptp_implies, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   363
             | (false, s) =>
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   364
               if is_tptp_equal s then (`I tptp_equal, [])
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   365
               else (proxy_base |>> prefix const_prefix, T_args)
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   366
             | _ => (name, [])
42569
5737947e4c77 make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents: 42568
diff changeset
   367
           else
42574
blanchet
parents: 42573
diff changeset
   368
             (proxy_base |>> prefix const_prefix, T_args)
blanchet
parents: 42573
diff changeset
   369
          | NONE => (name, T_args))
blanchet
parents: 42573
diff changeset
   370
        |> (fn (name, T_args) => CombConst (name, T, T_args))
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   371
      | intro _ tm = tm
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   372
  in intro true end
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   373
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   374
fun combformula_from_prop thy format type_sys eq_as_iff =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   375
  let
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   376
    fun do_term bs t atomic_types =
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   377
      combterm_from_term thy bs (Envir.eta_contract t)
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   378
      |>> (introduce_proxies format type_sys #> AAtom)
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   379
      ||> union (op =) atomic_types
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   380
    fun do_quant bs q s T t' =
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   381
      let val s = Name.variant (map fst bs) s in
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   382
        do_formula ((s, T) :: bs) t'
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   383
        #>> mk_aquant q [(`make_bound_var s, SOME T)]
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   384
      end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   385
    and do_conn bs c t1 t2 =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   386
      do_formula bs t1 ##>> do_formula bs t2
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   387
      #>> uncurry (mk_aconn c)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   388
    and do_formula bs t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   389
      case t of
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   390
        @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   391
      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   392
        do_quant bs AForall s T t'
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   393
      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   394
        do_quant bs AExists s T t'
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   395
      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   396
      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38752
diff changeset
   397
      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   398
      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   399
        if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   400
      | _ => do_term bs t
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   401
  in do_formula [] end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   402
42750
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   403
fun presimplify_term ctxt =
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   404
  Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   405
  #> Meson.presimplify ctxt
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   406
  #> prop_of
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   407
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41406
diff changeset
   408
fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   409
fun conceal_bounds Ts t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   410
  subst_bounds (map (Free o apfst concealed_bound_name)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   411
                    (0 upto length Ts - 1 ~~ Ts), t)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   412
fun reveal_bounds Ts =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   413
  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   414
                    (0 upto length Ts - 1 ~~ Ts))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   415
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   416
fun extensionalize_term ctxt t =
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   417
  let val thy = Proof_Context.theory_of ctxt in
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   418
    t |> cterm_of thy |> Meson.extensionalize_conv ctxt
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   419
      |> prop_of |> Logic.dest_equals |> snd
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   420
  end
38608
01ed56c46259 beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents: 38606
diff changeset
   421
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   422
fun introduce_combinators_in_term ctxt kind t =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   423
  let val thy = Proof_Context.theory_of ctxt in
38491
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   424
    if Meson.is_fol_term thy t then
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   425
      t
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   426
    else
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   427
      let
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   428
        fun aux Ts t =
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   429
          case t of
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   430
            @{const Not} $ t1 => @{const Not} $ aux Ts t1
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   431
          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   432
            t0 $ Abs (s, T, aux (T :: Ts) t')
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38618
diff changeset
   433
          | (t0 as Const (@{const_name All}, _)) $ t1 =>
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38618
diff changeset
   434
            aux Ts (t0 $ eta_expand Ts t1 1)
38491
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   435
          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   436
            t0 $ Abs (s, T, aux (T :: Ts) t')
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38618
diff changeset
   437
          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38618
diff changeset
   438
            aux Ts (t0 $ eta_expand Ts t1 1)
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   439
          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   440
          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38752
diff changeset
   441
          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   442
          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
38491
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   443
              $ t1 $ t2 =>
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   444
            t0 $ aux Ts t1 $ aux Ts t2
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   445
          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   446
                   t
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   447
                 else
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   448
                   t |> conceal_bounds Ts
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   449
                     |> Envir.eta_contract
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   450
                     |> cterm_of thy
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39886
diff changeset
   451
                     |> Meson_Clausify.introduce_combinators_in_cterm
38491
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   452
                     |> prop_of |> Logic.dest_equals |> snd
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   453
                     |> reveal_bounds Ts
39370
f8292d3020db use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents: 39005
diff changeset
   454
        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
38491
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   455
      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   456
      handle THM _ =>
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   457
             (* A type variable of sort "{}" will make abstraction fail. *)
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   458
             if kind = Conjecture then HOLogic.false_const
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   459
             else HOLogic.true_const
38491
f7e51d981a9f invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents: 38282
diff changeset
   460
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   461
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   462
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
42353
7797efa897a1 correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents: 42237
diff changeset
   463
   same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   464
fun freeze_term t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   465
  let
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   466
    fun aux (t $ u) = aux t $ aux u
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   467
      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   468
      | aux (Var ((s, i), T)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   469
        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   470
      | aux t = t
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   471
  in t |> exists_subterm is_Var t ? aux end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   472
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40145
diff changeset
   473
(* making fact and conjecture formulas *)
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   474
fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   475
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   476
    val thy = Proof_Context.theory_of ctxt
38608
01ed56c46259 beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents: 38606
diff changeset
   477
    val t = t |> Envir.beta_eta_contract
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   478
              |> transform_elim_prop
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41199
diff changeset
   479
              |> Object_Logic.atomize_term thy
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   480
    val need_trueprop = (fastype_of t = @{typ bool})
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38618
diff changeset
   481
    val t = t |> need_trueprop ? HOLogic.mk_Trueprop
42742
369dfc819056 unfold set constants in Sledgehammer/ATP as well if Metis does it too
blanchet
parents: 42734
diff changeset
   482
              |> Raw_Simplifier.rewrite_term thy
369dfc819056 unfold set constants in Sledgehammer/ATP as well if Metis does it too
blanchet
parents: 42734
diff changeset
   483
                     (Meson.unfold_set_const_simps ctxt) []
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   484
              |> extensionalize_term ctxt
42750
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   485
              |> presimp ? presimplify_term ctxt
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   486
              |> perhaps (try (HOLogic.dest_Trueprop))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   487
              |> introduce_combinators_in_term ctxt kind
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   488
              |> kind <> Axiom ? freeze_term
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   489
    val (combformula, atomic_types) =
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   490
      combformula_from_prop thy format type_sys eq_as_iff t []
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   491
  in
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   492
    {name = name, locality = loc, kind = kind, combformula = combformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   493
     atomic_types = atomic_types}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   494
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   495
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   496
fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   497
              ((name, loc), t) =
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   498
  case (keep_trivial,
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   499
        make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of
43001
f3492698dfc7 fixed trivial fact detection
blanchet
parents: 43000
diff changeset
   500
    (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
f3492698dfc7 fixed trivial fact detection
blanchet
parents: 43000
diff changeset
   501
    if s = tptp_true then NONE else SOME formula
41990
7f2793d51efc add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents: 41770
diff changeset
   502
  | (_, formula) => SOME formula
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   503
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   504
fun make_conjecture ctxt format prem_kind type_sys ts =
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   505
  let val last = length ts - 1 in
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   506
    map2 (fn j => fn t =>
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   507
             let
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   508
               val (kind, maybe_negate) =
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   509
                 if j = last then
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   510
                   (Conjecture, I)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   511
                 else
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   512
                   (prem_kind,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   513
                    if prem_kind = Conjecture then update_combformula mk_anot
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   514
                    else I)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   515
              in
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   516
                t |> make_formula ctxt format type_sys true true
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   517
                                  (string_of_int j) General kind
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   518
                  |> maybe_negate
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   519
              end)
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   520
         (0 upto last) ts
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   521
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   522
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   523
(** Finite and infinite type inference **)
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   524
42886
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   525
fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   526
  | deep_freeze_atyp T = T
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   527
val deep_freeze_type = map_atyps deep_freeze_atyp
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   528
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   529
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   530
   dangerous because their "exhaust" properties can easily lead to unsound ATP
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   531
   proofs. On the other hand, all HOL infinite types can be given the same
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   532
   models in first-order logic (via Löwenheim-Skolem). *)
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   533
42886
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   534
fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   535
    exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   536
  | should_encode_type _ _ All_Types _ = true
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   537
  | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   538
  | should_encode_type _ _ _ _ = false
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   539
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   540
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   541
                             should_predicate_on_var T =
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   542
    (heaviness = Heavy orelse should_predicate_on_var ()) andalso
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   543
    should_encode_type ctxt nonmono_Ts level T
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   544
  | should_predicate_on_type _ _ _ _ _ = false
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   545
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   546
fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   547
    String.isPrefix bound_var_prefix s
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   548
  | is_var_or_bound_var (CombVar _) = true
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   549
  | is_var_or_bound_var _ = false
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   550
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   551
datatype tag_site = Top_Level | Eq_Arg | Elsewhere
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   552
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   553
fun should_tag_with_type _ _ _ Top_Level _ _ = false
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   554
  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   555
    (case heaviness of
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   556
       Heavy => should_encode_type ctxt nonmono_Ts level T
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   557
     | Light =>
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   558
       case (site, is_var_or_bound_var u) of
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   559
         (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   560
       | _ => false)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   561
  | should_tag_with_type _ _ _ _ _ _ = false
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   562
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   563
fun homogenized_type ctxt nonmono_Ts level =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   564
  let
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   565
    val should_encode = should_encode_type ctxt nonmono_Ts level
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   566
    fun homo 0 T = if should_encode T then T else homo_infinite_type
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   567
      | homo ary (Type (@{type_name fun}, [T1, T2])) =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   568
        homo 0 T1 --> homo (ary - 1) T2
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   569
      | homo _ _ = raise Fail "expected function type"
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   570
  in homo end
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   571
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   572
(** "hBOOL" and "hAPP" **)
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   573
42574
blanchet
parents: 42573
diff changeset
   574
type sym_info =
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   575
  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   576
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   577
fun add_combterm_syms_to_table ctxt explicit_apply =
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   578
  let
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   579
    fun consider_var_arity const_T var_T max_ary =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   580
      let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   581
        fun iter ary T =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   582
          if ary = max_ary orelse type_instance ctxt (var_T, T) then ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   583
          else iter (ary + 1) (range_type T)
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   584
      in iter 0 const_T end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   585
    fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   586
      let val (head, args) = strip_combterm_comb tm in
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   587
        (case head of
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   588
           CombConst ((s, _), T, _) =>
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   589
           if String.isPrefix bound_var_prefix s then
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   590
             if explicit_apply = NONE andalso can dest_funT T then
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   591
               let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   592
                 fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   593
                   {pred_sym = pred_sym,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   594
                    min_ary =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   595
                      fold (fn T' => consider_var_arity T' T) types min_ary,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   596
                    max_ary = max_ary, types = types}
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   597
                 val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   598
               in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   599
                 if pointer_eq (ho_var_Ts', ho_var_Ts) then accum
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   600
                 else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   601
               end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   602
             else
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   603
               accum
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   604
           else
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   605
             let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   606
               val ary = length args
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   607
             in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   608
               (ho_var_Ts,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   609
                case Symtab.lookup sym_tab s of
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   610
                  SOME {pred_sym, min_ary, max_ary, types} =>
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   611
                  let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   612
                    val types' = types |> insert_type ctxt I T
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   613
                    val min_ary =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   614
                      if is_some explicit_apply orelse
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   615
                         pointer_eq (types', types) then
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   616
                        min_ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   617
                      else
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   618
                        fold (consider_var_arity T) ho_var_Ts min_ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   619
                  in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   620
                    Symtab.update (s, {pred_sym = pred_sym andalso top_level,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   621
                                       min_ary = Int.min (ary, min_ary),
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   622
                                       max_ary = Int.max (ary, max_ary),
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   623
                                       types = types'})
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   624
                                  sym_tab
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   625
                  end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   626
                | NONE =>
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   627
                  let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   628
                    val min_ary =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   629
                      case explicit_apply of
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   630
                        SOME true => 0
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   631
                      | SOME false => ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   632
                      | NONE => fold (consider_var_arity T) ho_var_Ts ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   633
                  in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   634
                    Symtab.update_new (s, {pred_sym = top_level,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   635
                                           min_ary = min_ary, max_ary = ary,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   636
                                           types = [T]})
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   637
                                      sym_tab
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   638
                  end)
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   639
             end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   640
         | _ => accum)
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   641
        |> fold (add false) args
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   642
      end
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   643
  in add true end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   644
fun add_fact_syms_to_table ctxt explicit_apply =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   645
  fact_lift (formula_fold NONE
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   646
                          (K (add_combterm_syms_to_table ctxt explicit_apply)))
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   647
42675
223153bb68a1 added type annotation for SML/NJ
blanchet
parents: 42674
diff changeset
   648
val default_sym_table_entries : (string * sym_info) list =
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   649
  [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   650
   (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   651
   (make_fixed_const predicator_name,
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   652
    {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   653
  ([tptp_false, tptp_true]
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   654
   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   655
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   656
fun sym_table_for_facts ctxt explicit_apply facts =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   657
  Symtab.empty
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   658
  |> fold Symtab.default default_sym_table_entries
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   659
  |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   660
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   661
fun min_arity_of sym_tab s =
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   662
  case Symtab.lookup sym_tab s of
42574
blanchet
parents: 42573
diff changeset
   663
    SOME ({min_ary, ...} : sym_info) => min_ary
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   664
  | NONE =>
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   665
    case strip_prefix_and_unascii const_prefix s of
42547
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
   666
      SOME s =>
42570
77f94ac04f32 cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents: 42569
diff changeset
   667
      let val s = s |> unmangled_const_name |> invert_const in
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   668
        if s = predicator_name then 1
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   669
        else if s = app_op_name then 2
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   670
        else if s = type_pred_name then 1
42557
ae0deb39a254 fixed min-arity computation when "explicit_apply" is specified
blanchet
parents: 42556
diff changeset
   671
        else 0
42547
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
   672
      end
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   673
    | NONE => 0
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   674
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   675
(* True if the constant ever appears outside of the top-level position in
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   676
   literals, or if it appears with different arities (e.g., because of different
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   677
   type instantiations). If false, the constant always receives all of its
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   678
   arguments and is used as a predicate. *)
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   679
fun is_pred_sym sym_tab s =
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   680
  case Symtab.lookup sym_tab s of
42574
blanchet
parents: 42573
diff changeset
   681
    SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
blanchet
parents: 42573
diff changeset
   682
    pred_sym andalso min_ary = max_ary
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   683
  | NONE => false
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   684
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   685
val predicator_combconst =
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   686
  CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   687
fun predicator tm = CombApp (predicator_combconst, tm)
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   688
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   689
fun introduce_predicators_in_combterm sym_tab tm =
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   690
  case strip_combterm_comb tm of
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   691
    (CombConst ((s, _), _, _), _) =>
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   692
    if is_pred_sym sym_tab s then tm else predicator tm
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   693
  | _ => predicator tm
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   694
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   695
fun list_app head args = fold (curry (CombApp o swap)) args head
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   696
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   697
fun explicit_app arg head =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   698
  let
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   699
    val head_T = combtyp_of head
42693
3c2baf9b3c61 reverted 6efda6167e5d because unsound -- Vampire found a counterexample
blanchet
parents: 42691
diff changeset
   700
    val (arg_T, res_T) = dest_funT head_T
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   701
    val explicit_app =
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   702
      CombConst (`make_fixed_const app_op_name, head_T --> head_T,
42693
3c2baf9b3c61 reverted 6efda6167e5d because unsound -- Vampire found a counterexample
blanchet
parents: 42691
diff changeset
   703
                 [arg_T, res_T])
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   704
  in list_app explicit_app [head, arg] end
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   705
fun list_explicit_app head args = fold explicit_app args head
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   706
42565
93f58e6a6f3e proper handling of partially applied proxy symbols
blanchet
parents: 42564
diff changeset
   707
fun introduce_explicit_apps_in_combterm sym_tab =
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   708
  let
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   709
    fun aux tm =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   710
      case strip_combterm_comb tm of
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   711
        (head as CombConst ((s, _), _, _), args) =>
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   712
        args |> map aux
42557
ae0deb39a254 fixed min-arity computation when "explicit_apply" is specified
blanchet
parents: 42556
diff changeset
   713
             |> chop (min_arity_of sym_tab s)
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   714
             |>> list_app head
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   715
             |-> list_explicit_app
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   716
      | (head, args) => list_explicit_app head (map aux args)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   717
  in aux end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   718
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   719
fun chop_fun 0 T = ([], T)
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   720
  | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   721
    chop_fun (n - 1) ran_T |>> cons dom_T
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   722
  | chop_fun _ _ = raise Fail "unexpected non-function"
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   723
42780
be6164bc9744 avoid "UnequalLengths" exception for special constant "fequal" -- and optimize code in the common case where no type arguments are needed
blanchet
parents: 42778
diff changeset
   724
fun filter_type_args _ _ _ [] = []
be6164bc9744 avoid "UnequalLengths" exception for special constant "fequal" -- and optimize code in the common case where no type arguments are needed
blanchet
parents: 42778
diff changeset
   725
  | filter_type_args thy s arity T_args =
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   726
    let
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   727
      (* will throw "TYPE" for pseudo-constants *)
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   728
      val U = if s = app_op_name then
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   729
                @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   730
              else
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   731
                s |> Sign.the_const_type thy
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   732
    in
42781
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   733
      case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   734
        [] => []
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   735
      | res_U_vars =>
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   736
        let val U_args = (s, U) |> Sign.const_typargs thy in
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   737
          U_args ~~ T_args
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   738
          |> map_filter (fn (U, T) =>
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   739
                            if member (op =) res_U_vars (dest_TVar U) then
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   740
                              SOME T
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   741
                            else
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   742
                              NONE)
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   743
        end
42780
be6164bc9744 avoid "UnequalLengths" exception for special constant "fequal" -- and optimize code in the common case where no type arguments are needed
blanchet
parents: 42778
diff changeset
   744
    end
be6164bc9744 avoid "UnequalLengths" exception for special constant "fequal" -- and optimize code in the common case where no type arguments are needed
blanchet
parents: 42778
diff changeset
   745
    handle TYPE _ => T_args
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   746
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   747
fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   748
  let
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   749
    val thy = Proof_Context.theory_of ctxt
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   750
    fun aux arity (CombApp (tm1, tm2)) =
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   751
        CombApp (aux (arity + 1) tm1, aux 0 tm2)
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   752
      | aux arity (CombConst (name as (s, _), T, T_args)) =
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   753
        let
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   754
          val level = level_of_type_sys type_sys
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   755
          val (T, T_args) =
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   756
            (* Aggressively merge most "hAPPs" if the type system is unsound
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   757
               anyway, by distinguishing overloads only on the homogenized
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   758
               result type. Don't do it for lightweight type systems, though,
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   759
               since it leads to too many unsound proofs. *)
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   760
            if s = const_prefix ^ app_op_name andalso
42726
70fc448a1815 avoid "Empty" exception by making sure that a certain optimization only is attempted when it makes sense
blanchet
parents: 42722
diff changeset
   761
               length T_args = 2 andalso
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   762
               not (is_type_sys_virtually_sound type_sys) andalso
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   763
               heaviness_of_type_sys type_sys = Heavy then
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   764
              T_args |> map (homogenized_type ctxt nonmono_Ts level 0)
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   765
                     |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   766
                                    (T --> T, tl Ts)
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   767
                                  end)
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   768
            else
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   769
              (T, T_args)
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   770
        in
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   771
          (case strip_prefix_and_unascii const_prefix s of
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   772
             NONE => (name, T_args)
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   773
           | SOME s'' =>
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   774
             let
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   775
               val s'' = invert_const s''
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   776
               fun filtered_T_args false = T_args
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   777
                 | filtered_T_args true = filter_type_args thy s'' arity T_args
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   778
             in
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   779
               case type_arg_policy type_sys s'' of
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   780
                 Explicit_Type_Args drop_args =>
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   781
                 (name, filtered_T_args drop_args)
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   782
               | Mangled_Type_Args drop_args =>
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   783
                 (mangled_const_name (filtered_T_args drop_args) name, [])
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   784
               | No_Type_Args => (name, [])
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   785
             end)
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   786
          |> (fn (name, T_args) => CombConst (name, T, T_args))
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   787
        end
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   788
      | aux _ tm = tm
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   789
  in aux 0 end
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   790
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   791
fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   792
  not (is_setting_higher_order format type_sys)
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   793
  ? (introduce_explicit_apps_in_combterm sym_tab
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   794
     #> introduce_predicators_in_combterm sym_tab)
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   795
  #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   796
fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   797
  update_combformula (formula_map
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   798
      (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   799
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   800
(** Helper facts **)
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   801
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   802
fun ti_ti_helper_fact () =
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   803
  let
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   804
    fun var s = ATerm (`I s, [])
42589
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
   805
    fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   806
  in
42612
bb9143d7e217 cosmetics
blanchet
parents: 42608
diff changeset
   807
    Formula (helper_prefix ^ "ti_ti", Axiom,
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   808
             AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))
42879
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   809
             |> close_formula_universally, simp_info, NONE)
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   810
  end
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   811
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   812
fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   813
  case strip_prefix_and_unascii const_prefix s of
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   814
    SOME mangled_s =>
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   815
    let
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   816
      val thy = Proof_Context.theory_of ctxt
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   817
      val unmangled_s = mangled_s |> unmangled_const_name
42893
fd4babefe3f2 prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents: 42886
diff changeset
   818
      fun dub_and_inst c needs_fairly_sound (th, j) =
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   819
        ((c ^ "_" ^ string_of_int j ^
42893
fd4babefe3f2 prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents: 42886
diff changeset
   820
          (if needs_fairly_sound then typed_helper_suffix
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   821
           else untyped_helper_suffix),
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   822
          General),
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   823
         let val t = th |> prop_of in
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   824
           t |> ((case general_type_arg_policy type_sys of
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   825
                    Mangled_Type_Args _ => true
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   826
                  | _ => false) andalso
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   827
                 not (null (Term.hidden_polymorphism t)))
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   828
                ? (case types of
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   829
                     [T] => specialize_type thy (invert_const unmangled_s, T)
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   830
                   | _ => I)
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   831
         end)
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   832
      fun make_facts eq_as_iff =
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   833
        map_filter (make_fact ctxt format type_sys false eq_as_iff false)
42893
fd4babefe3f2 prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents: 42886
diff changeset
   834
      val fairly_sound = is_type_sys_fairly_sound type_sys
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   835
    in
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   836
      metis_helpers
42894
ce269ee43800 further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents: 42893
diff changeset
   837
      |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   838
                  if metis_s <> unmangled_s orelse
42894
ce269ee43800 further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents: 42893
diff changeset
   839
                     (needs_fairly_sound andalso not fairly_sound) then
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   840
                    []
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   841
                  else
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   842
                    ths ~~ (1 upto length ths)
42893
fd4babefe3f2 prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents: 42886
diff changeset
   843
                    |> map (dub_and_inst mangled_s needs_fairly_sound)
fd4babefe3f2 prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents: 42886
diff changeset
   844
                    |> make_facts (not needs_fairly_sound))
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   845
    end
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   846
  | NONE => []
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   847
fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   848
  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   849
                  []
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   850
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   851
fun translate_atp_fact ctxt format type_sys keep_trivial =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   852
  `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of)
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   853
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   854
fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   855
                       rich_facts =
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   856
  let
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   857
    val thy = Proof_Context.theory_of ctxt
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   858
    val fact_ts = map (prop_of o snd o snd) rich_facts
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   859
    val (facts, fact_names) =
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   860
      rich_facts
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   861
      |> map_filter (fn (NONE, _) => NONE
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   862
                      | (SOME fact, (name, _)) => SOME (fact, name))
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   863
      |> ListPair.unzip
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   864
    (* Remove existing facts from the conjecture, as this can dramatically
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   865
       boost an ATP's performance (for some reason). *)
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   866
    val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   867
    val goal_t = Logic.list_implies (hyp_ts, concl_t)
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   868
    val all_ts = goal_t :: fact_ts
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   869
    val subs = tfree_classes_of_terms all_ts
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   870
    val supers = tvar_classes_of_terms all_ts
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   871
    val tycons = type_consts_of_terms thy all_ts
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   872
    val conjs =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   873
      hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   874
    val (supers', arity_clauses) =
42589
9f7c48463645 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents: 42586
diff changeset
   875
      if level_of_type_sys type_sys = No_Types then ([], [])
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   876
      else make_arity_clauses thy tycons supers
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   877
    val class_rel_clauses = make_class_rel_clauses thy subs supers'
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   878
  in
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   879
    (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   880
  end
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   881
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   882
fun fo_literal_from_type_literal (TyLitVar (class, name)) =
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   883
    (true, ATerm (class, [ATerm (name, [])]))
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   884
  | fo_literal_from_type_literal (TyLitFree (class, name)) =
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   885
    (true, ATerm (class, [ATerm (name, [])]))
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   886
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   887
fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   888
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   889
fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   890
  CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T])
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   891
           |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   892
           tm)
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   893
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   894
fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   895
  | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   896
    accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   897
fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   898
  | is_var_nonmonotonic_in_formula pos phi _ name =
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   899
    formula_fold pos (var_occurs_positively_naked_in_term name) phi false
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   900
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   901
fun mk_const_aterm x T_args args =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   902
  ATerm (x, map (fo_term_from_typ false) T_args @ args)
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   903
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   904
fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   905
  CombConst (`make_fixed_const type_tag_name, T --> T, [T])
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   906
  |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   907
  |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   908
  |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   909
and term_from_combterm ctxt format nonmono_Ts type_sys =
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   910
  let
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   911
    fun aux site u =
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   912
      let
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   913
        val (head, args) = strip_combterm_comb u
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   914
        val (x as (s, _), T_args) =
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   915
          case head of
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   916
            CombConst (name, _, T_args) => (name, T_args)
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   917
          | CombVar (name, _) => (name, [])
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   918
          | CombApp _ => raise Fail "impossible \"CombApp\""
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   919
        val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   920
                       else Elsewhere
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   921
        val t = mk_const_aterm x T_args (map (aux arg_site) args)
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   922
        val T = combtyp_of u
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   923
      in
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   924
        t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   925
                tag_with_type ctxt format nonmono_Ts type_sys T
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   926
              else
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   927
                I)
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   928
      end
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   929
  in aux end
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   930
and formula_from_combformula ctxt format nonmono_Ts type_sys
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   931
                             should_predicate_on_var =
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   932
  let
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   933
    val higher_order = is_setting_higher_order format type_sys
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   934
    val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   935
    val do_bound_type =
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   936
      case type_sys of
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   937
        Simple_Types level =>
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   938
        homogenized_type ctxt nonmono_Ts level 0
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   939
        #> mangled_type higher_order false 0 #> SOME
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   940
      | _ => K NONE
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   941
    fun do_out_of_bound_type pos phi universal (name, T) =
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   942
      if should_predicate_on_type ctxt nonmono_Ts type_sys
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   943
             (fn () => should_predicate_on_var pos phi universal name) T then
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   944
        CombVar (name, T)
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   945
        |> type_pred_combterm ctxt nonmono_Ts type_sys T
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   946
        |> do_term |> AAtom |> SOME
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   947
      else
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   948
        NONE
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   949
    fun do_formula pos (AQuant (q, xs, phi)) =
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   950
        let
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   951
          val phi = phi |> do_formula pos
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   952
          val universal = Option.map (q = AExists ? not) pos
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   953
        in
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   954
          AQuant (q, xs |> map (apsnd (fn NONE => NONE
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   955
                                        | SOME T => do_bound_type T)),
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   956
                  (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   957
                      (map_filter
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   958
                           (fn (_, NONE) => NONE
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   959
                             | (s, SOME T) =>
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   960
                               do_out_of_bound_type pos phi universal (s, T))
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   961
                           xs)
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   962
                      phi)
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   963
        end
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   964
      | do_formula pos (AConn conn) = aconn_map pos do_formula conn
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   965
      | do_formula _ (AAtom tm) = AAtom (do_term tm)
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   966
  in do_formula o SOME end
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   967
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
   968
fun bound_atomic_types format type_sys Ts =
42727
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   969
  mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
   970
                (atp_type_literals_for_types format type_sys Axiom Ts))
42727
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   971
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
   972
fun formula_for_fact ctxt format nonmono_Ts type_sys
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   973
                     ({combformula, atomic_types, ...} : translated_formula) =
42727
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   974
  combformula
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   975
  |> close_combformula_universally
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   976
  |> formula_from_combformula ctxt format nonmono_Ts type_sys
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   977
                              is_var_nonmonotonic_in_formula true
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
   978
  |> bound_atomic_types format type_sys atomic_types
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   979
  |> close_formula_universally
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   980
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   981
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   982
   of monomorphization). The TPTP explicitly forbids name clashes, and some of
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   983
   the remote provers might care. *)
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
   984
fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   985
                          (j, formula as {name, locality, kind, ...}) =
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   986
  Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   987
                     else string_of_int j ^ "_") ^
42647
59142dbfa3ba no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
blanchet
parents: 42646
diff changeset
   988
           ascii_of name,
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
   989
           kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
42879
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   990
           case locality of
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   991
             Intro => intro_info
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   992
           | Elim => elim_info
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   993
           | Simp => simp_info
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   994
           | _ => NONE)
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   995
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42895
diff changeset
   996
fun formula_line_for_class_rel_clause
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42895
diff changeset
   997
        (ClassRelClause {name, subclass, superclass, ...}) =
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   998
  let val ty_arg = ATerm (`I "T", []) in
42577
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42576
diff changeset
   999
    Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1000
             AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1001
                               AAtom (ATerm (superclass, [ty_arg]))])
42879
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
  1002
             |> close_formula_universally, intro_info, NONE)
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1003
  end
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1004
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1005
fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1006
    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1007
  | fo_literal_from_arity_literal (TVarLit (c, sort)) =
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1008
    (false, ATerm (c, [ATerm (sort, [])]))
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1009
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42895
diff changeset
  1010
fun formula_line_for_arity_clause
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42895
diff changeset
  1011
        (ArityClause {name, prem_lits, concl_lits, ...}) =
42577
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42576
diff changeset
  1012
  Formula (arity_clause_prefix ^ ascii_of name, Axiom,
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1013
           mk_ahorn (map (formula_from_fo_literal o apfst not
42895
c8d9bce88f89 name tuning
blanchet
parents: 42894
diff changeset
  1014
                          o fo_literal_from_arity_literal) prem_lits)
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1015
                    (formula_from_fo_literal
42895
c8d9bce88f89 name tuning
blanchet
parents: 42894
diff changeset
  1016
                         (fo_literal_from_arity_literal concl_lits))
42879
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
  1017
           |> close_formula_universally, intro_info, NONE)
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1018
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
  1019
fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1020
        ({name, kind, combformula, ...} : translated_formula) =
42577
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42576
diff changeset
  1021
  Formula (conjecture_prefix ^ name, kind,
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
  1022
           formula_from_combformula ctxt format nonmono_Ts type_sys
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42895
diff changeset
  1023
               is_var_nonmonotonic_in_formula false
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42895
diff changeset
  1024
               (close_combformula_universally combformula)
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1025
           |> close_formula_universally, NONE, NONE)
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1026
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
  1027
fun free_type_literals format type_sys
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
  1028
                       ({atomic_types, ...} : translated_formula) =
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
  1029
  atomic_types |> atp_type_literals_for_types format type_sys Conjecture
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1030
               |> map fo_literal_from_type_literal
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1031
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1032
fun formula_line_for_free_type j lit =
42577
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42576
diff changeset
  1033
  Formula (tfree_prefix ^ string_of_int j, Hypothesis,
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1034
           formula_from_fo_literal lit, NONE, NONE)
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
  1035
fun formula_lines_for_free_types format type_sys facts =
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1036
  let
42956
9aeb0f6ad971 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents: 42951
diff changeset
  1037
    val litss = map (free_type_literals format type_sys) facts
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1038
    val lits = fold (union (op =)) litss []
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1039
  in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1040
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1041
(** Symbol declarations **)
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
  1042
42574
blanchet
parents: 42573
diff changeset
  1043
fun should_declare_sym type_sys pred_sym s =
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
  1044
  is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
42894
ce269ee43800 further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents: 42893
diff changeset
  1045
  (case type_sys of
ce269ee43800 further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents: 42893
diff changeset
  1046
     Simple_Types _ => true
ce269ee43800 further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents: 42893
diff changeset
  1047
   | Tags (_, _, Light) => true
ce269ee43800 further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents: 42893
diff changeset
  1048
   | _ => not pred_sym)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1049
42886
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
  1050
fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
42574
blanchet
parents: 42573
diff changeset
  1051
  let
42698
ffd1ae4ff5c6 help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents: 42697
diff changeset
  1052
    fun add_combterm in_conj tm =
42574
blanchet
parents: 42573
diff changeset
  1053
      let val (head, args) = strip_combterm_comb tm in
blanchet
parents: 42573
diff changeset
  1054
        (case head of
<