src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
author blanchet
Thu, 19 May 2011 10:24:13 +0200
changeset 42854 d99167ac4f8a
parent 42852 40649ab0cead
child 42855 b48529f41888
permissions -rw-r--r--
since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
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
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
    12
  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
    13
  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
    14
  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
    15
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
  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
    17
  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
    18
    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
    19
  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
    20
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
  datatype type_system =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
    22
    Simple_Types of type_level |
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    23
    Preds of polymorphism * type_level * type_heaviness |
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    24
    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
    25
40114
blanchet
parents: 40069
diff changeset
    26
  type translated_formula
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    27
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
    28
  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
    29
  val fact_prefix : string
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    30
  val conjecture_prefix : string
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    31
  val predicator_base : string
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
    32
  val explicit_app_base : string
42549
b9754f26c7bc handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents: 42548
diff changeset
    33
  val type_pred_base : string
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
    34
  val tff_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
    35
  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
    36
  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
    37
  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
    38
  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
    39
  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
    40
  val unmangled_const : string -> string * string fo_term list
41088
54eb8e7c7f9b clarified terminology
blanchet
parents: 40204
diff changeset
    41
  val translate_atp_fact :
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    42
    Proof.context -> bool -> (string * locality) * thm
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    43
    -> translated_formula option * ((string * locality) * thm)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39975
diff changeset
    44
  val prepare_atp_problem :
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
    45
    Proof.context -> formula_kind -> formula_kind -> type_system -> bool
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
    46
    -> term list -> term
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
    47
    -> (translated_formula option * ((string * 'a) * thm)) list
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
    48
    -> string problem * string Symtab.table * int * int
42755
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42754
diff changeset
    49
       * (string * 'a) list vector * int Symtab.table
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
    50
  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
    51
end;
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    52
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
    53
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
    54
struct
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    55
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    56
open ATP_Problem
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39452
diff changeset
    57
open Metis_Translate
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    58
open Sledgehammer_Util
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    59
open Sledgehammer_Filter
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    60
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    61
(* experimental *)
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    62
val generate_useful_info = false
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    63
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    64
(* 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
    65
   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
    66
   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
    67
   readable. For these reason, they are enabled by default. *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
    68
val readable_names =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
    69
  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
    70
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    71
val type_decl_prefix = "type_"
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    72
val sym_decl_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
    73
val fact_prefix = "fact_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    74
val conjecture_prefix = "conj_"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    75
val helper_prefix = "help_"
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    76
val class_rel_clause_prefix = "crel_";
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    77
val arity_clause_prefix = "arity_"
39975
7c50d5ca5c04 avoid generating several formulas with the same name ("tfrees")
blanchet
parents: 39954
diff changeset
    78
val tfree_prefix = "tfree_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    79
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    80
val predicator_base = "hBOOL"
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
    81
val explicit_app_base = "hAPP"
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
    82
val type_pred_base = "is"
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
    83
val tff_type_prefix = "ty_"
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
    84
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
    85
fun make_tff_type s = tff_type_prefix ^ ascii_of s
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
    86
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    87
(* Freshness almost guaranteed! *)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    88
val sledgehammer_weak_prefix = "Sledgehammer:"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    89
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
    90
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
    91
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
    92
  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
    93
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
    94
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
    95
datatype type_system =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
    96
  Simple_Types of type_level |
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    97
  Preds of polymorphism * type_level * type_heaviness |
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    98
  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
    99
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   100
fun try_unsuffixes ss s =
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   101
  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
   102
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
   103
fun type_sys_from_string s =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   104
  (case try (unprefix "poly_") s of
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   105
     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
   106
   | 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
   107
     case try (unprefix "mono_") s of
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   108
       SOME s => (SOME Monomorphic, s)
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   109
     | NONE =>
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   110
       case try (unprefix "mangled_") s of
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   111
         SOME s => (SOME Mangled_Monomorphic, s)
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   112
       | 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
   113
  ||> (fn s =>
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   114
          (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   115
          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
   116
            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
   117
          | NONE =>
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   118
            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
   119
              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
   120
            | NONE => (All_Types, s))
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   121
  ||> apsnd (fn s =>
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   122
                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
   123
                  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
   124
                | NONE => (Light, s))
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   125
  |> (fn (poly, (level, (heaviness, core))) =>
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   126
         case (core, (poly, level, heaviness)) 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
   127
           ("simple_types", (NONE, _, Light)) => Simple_Types level
42851
3bb63850488b removed "poly_tags_light_bang" since highly unsound
blanchet
parents: 42837
diff changeset
   128
         | ("preds", (SOME Polymorphic, _, _)) =>
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
   129
           if level = All_Types then Preds (Polymorphic, 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
   130
           else raise Same.SAME
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
   131
         | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
42851
3bb63850488b removed "poly_tags_light_bang" since highly unsound
blanchet
parents: 42837
diff changeset
   132
         | ("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
   133
           Tags (Polymorphic, All_Types, heaviness)
42851
3bb63850488b removed "poly_tags_light_bang" since highly unsound
blanchet
parents: 42837
diff changeset
   134
         | ("tags", (SOME Polymorphic, Finite_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
   135
           (* The light encoding yields too many unsound proofs. *)
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
   136
           Tags (Polymorphic, Finite_Types, Heavy)
42851
3bb63850488b removed "poly_tags_light_bang" since highly unsound
blanchet
parents: 42837
diff changeset
   137
         | ("tags", (SOME Polymorphic, _, _)) => raise Same.SAME
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
   138
         | ("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
   139
         | ("args", (SOME poly, All_Types (* naja *), Light)) =>
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   140
           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
   141
         | ("erased", (NONE, All_Types (* naja *), Light)) =>
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   142
           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
   143
         | _ => 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
   144
  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
   145
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   146
fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   147
  | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   148
  | 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
   149
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   150
fun level_of_type_sys (Simple_Types level) = level
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   151
  | level_of_type_sys (Preds (_, level, _)) = level
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   152
  | level_of_type_sys (Tags (_, level, _)) = level
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   153
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   154
fun heaviness_of_type_sys (Simple_Types _) = Heavy
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   155
  | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   156
  | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   157
42687
blanchet
parents: 42685
diff changeset
   158
fun is_type_level_virtually_sound level =
blanchet
parents: 42685
diff changeset
   159
  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
   160
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
   161
  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
   162
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
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
   164
  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
   165
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
   166
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
   167
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
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
   168
  | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
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
   169
  | formula_map f (AAtom tm) = AAtom (f 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
   170
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   171
fun formula_fold pos f =
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
   172
  let
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   173
    fun aux pos (AQuant (_, _, phi)) = aux pos phi
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   174
      | aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi
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
   175
      | aux pos (AConn (AImplies, [phi1, phi2])) =
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   176
        aux (Option.map not pos) phi1 #> aux pos phi2
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   177
      | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   178
      | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   179
      | aux _ (AConn (_, phis)) = fold (aux NONE) phis
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
   180
      | aux pos (AAtom tm) = f pos tm
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   181
  in aux pos 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
   182
40114
blanchet
parents: 40069
diff changeset
   183
type translated_formula =
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38748
diff changeset
   184
  {name: string,
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   185
   locality: locality,
42525
7a506b0b644f distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree
blanchet
parents: 42524
diff changeset
   186
   kind: formula_kind,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   187
   combformula: (name, typ, combterm) formula,
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   188
   atomic_types: typ list}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   189
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   190
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
   191
                          : translated_formula) =
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   192
  {name = name, locality = locality, kind = kind, combformula = f combformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   193
   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
   194
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
   195
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
   196
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
   197
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
   198
(* 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
   199
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
   200
  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
   201
  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
   202
  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
   203
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   204
fun should_drop_arg_type_args (Simple_Types _) =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   205
    false (* since TFF doesn't support overloading *)
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   206
  | should_drop_arg_type_args type_sys =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   207
    level_of_type_sys type_sys = All_Types andalso
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   208
    heaviness_of_type_sys type_sys = Heavy
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   209
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
   210
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
   211
  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
   212
    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
   213
  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
   214
    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
   215
  else
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   216
    Explicit_Type_Args (should_drop_arg_type_args type_sys)
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   217
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   218
fun type_arg_policy _ @{const_name HOL.eq} = No_Type_Args
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   219
  | type_arg_policy type_sys _ = 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
   220
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
   221
fun atp_type_literals_for_types type_sys kind Ts =
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
  if level_of_type_sys type_sys = No_Types 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
   223
    []
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
   224
  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
   225
    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
   226
       |> 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
   227
                   | 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
   228
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   229
fun mk_anot phi = AConn (ANot, [phi])
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   230
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
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
   231
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
   232
  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
   233
    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
   234
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   235
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
   236
  | 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
   237
fun mk_aquant _ [] phi = phi
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   238
  | 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
   239
    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
   240
  | 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
   241
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   242
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
   243
  let
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   244
    fun formula_vars bounds (AQuant (_, xs, phi)) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   245
        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
   246
      | 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
   247
      | formula_vars bounds (AAtom tm) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   248
        union (op =) (atom_vars tm []
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   249
                      |> 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
   250
  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
   251
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   252
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
   253
  | combterm_vars (CombConst _) = I
42574
blanchet
parents: 42573
diff changeset
   254
  | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   255
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
   256
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   257
fun term_vars (ATerm (name as (s, _), tms)) =
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   258
  is_atp_variable s ? insert (op =) (name, NONE)
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   259
  #> fold term_vars tms
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   260
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
   261
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   262
fun fo_term_from_typ (Type (s, Ts)) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   263
    ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts)
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   264
  | fo_term_from_typ (TFree (s, _)) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   265
    ATerm (`make_fixed_type_var s, [])
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   266
  | fo_term_from_typ (TVar ((x as (s, _)), _)) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   267
    ATerm ((make_schematic_type_var x, s), [])
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   268
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   269
(* 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
   270
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
   271
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   272
fun generic_mangled_type_name f (ATerm (name, [])) = f name
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   273
  | 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
   274
    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
   275
    ^ ")"
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   276
val mangled_type_name =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   277
  fo_term_from_typ
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   278
  #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   279
                generic_mangled_type_name snd ty))
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
   280
42574
blanchet
parents: 42573
diff changeset
   281
fun generic_mangled_type_suffix f g Ts =
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
   282
  fold_rev (curry (op ^) o g o prefix mangled_type_sep
42574
blanchet
parents: 42573
diff changeset
   283
            o generic_mangled_type_name f) Ts ""
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   284
fun mangled_const_name T_args (s, s') =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   285
  let val ty_args = map fo_term_from_typ T_args in
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   286
    (s ^ generic_mangled_type_suffix fst ascii_of ty_args,
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   287
     s' ^ generic_mangled_type_suffix snd I ty_args)
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   288
  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
   289
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
   290
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
   291
  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
   292
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
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
   294
  (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
   295
   -- 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
   296
                    [] >> 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
   297
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
   298
  (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
   299
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
   300
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
   301
  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
   302
    |> 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
   303
           (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
   304
                                                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
   305
    |> 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
   306
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   307
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
   308
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
   309
  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
   310
    (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
   311
  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
   312
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   313
fun introduce_proxies tm =
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   314
  let
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   315
    fun aux top_level (CombApp (tm1, tm2)) =
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   316
        CombApp (aux top_level tm1, aux false tm2)
42574
blanchet
parents: 42573
diff changeset
   317
      | aux top_level (CombConst (name as (s, 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
   318
        (case proxify_const s of
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   319
           SOME proxy_base =>
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   320
           if top_level then
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   321
             (case s of
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   322
                "c_False" => (tptp_false, s')
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   323
              | "c_True" => (tptp_true, s')
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   324
              | _ => name, [])
42569
5737947e4c77 make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents: 42568
diff changeset
   325
           else
42574
blanchet
parents: 42573
diff changeset
   326
             (proxy_base |>> prefix const_prefix, T_args)
blanchet
parents: 42573
diff changeset
   327
          | NONE => (name, T_args))
blanchet
parents: 42573
diff changeset
   328
        |> (fn (name, T_args) => CombConst (name, T, T_args))
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   329
      | aux _ tm = tm
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   330
  in aux true tm end
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   331
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   332
fun combformula_from_prop thy eq_as_iff =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   333
  let
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   334
    fun do_term bs t atomic_types =
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   335
      combterm_from_term thy bs (Envir.eta_contract t)
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   336
      |>> (introduce_proxies #> AAtom)
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   337
      ||> union (op =) atomic_types
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   338
    fun do_quant bs q s T t' =
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   339
      let val s = Name.variant (map fst bs) s in
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   340
        do_formula ((s, T) :: bs) t'
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   341
        #>> mk_aquant q [(`make_bound_var s, SOME T)]
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   342
      end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   343
    and do_conn bs c t1 t2 =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   344
      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
   345
      #>> uncurry (mk_aconn c)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   346
    and do_formula bs t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   347
      case t of
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   348
        @{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
   349
      | 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
   350
        do_quant bs AForall s T t'
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   351
      | 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
   352
        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
   353
      | @{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
   354
      | @{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
   355
      | @{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
   356
      | 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
   357
        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
   358
      | _ => do_term bs t
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   359
  in do_formula [] end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   360
42750
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   361
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
   362
  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
   363
  #> 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
   364
  #> prop_of
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   365
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41406
diff changeset
   366
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
   367
fun conceal_bounds Ts t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   368
  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
   369
                    (0 upto length Ts - 1 ~~ Ts), t)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   370
fun reveal_bounds Ts =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   371
  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
   372
                    (0 upto length Ts - 1 ~~ Ts))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   373
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
   374
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
   375
  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
   376
    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
   377
      |> 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
   378
  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
   379
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   380
fun introduce_combinators_in_term ctxt kind t =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   381
  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
   382
    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
   383
      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
   384
    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
   385
      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
   386
        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
   387
          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
   388
            @{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
   389
          | (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
   390
            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
   391
          | (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
   392
            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
   393
          | (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
   394
            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
   395
          | (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
   396
            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
   397
          | (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
   398
          | (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
   399
          | (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
   400
          | (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
   401
              $ 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
   402
            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
   403
          | _ => 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
   404
                   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
   405
                 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
   406
                   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
   407
                     |> 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
   408
                     |> cterm_of thy
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39886
diff changeset
   409
                     |> 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
   410
                     |> 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
   411
                     |> reveal_bounds Ts
39370
f8292d3020db use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents: 39005
diff changeset
   412
        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
   413
      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
   414
      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
   415
             (* 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
   416
             if kind = Conjecture then HOLogic.false_const
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   417
             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
   418
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   419
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   420
(* 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
   421
   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
   422
fun freeze_term t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   423
  let
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   424
    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
   425
      | 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
   426
      | aux (Var ((s, i), T)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   427
        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
   428
      | aux t = t
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   429
  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
   430
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
   431
(* making fact and conjecture formulas *)
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   432
fun make_formula ctxt 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
   433
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   434
    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
   435
    val t = t |> Envir.beta_eta_contract
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38618
diff changeset
   436
              |> transform_elim_term
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41199
diff changeset
   437
              |> Object_Logic.atomize_term thy
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   438
    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
   439
    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
   440
              |> Raw_Simplifier.rewrite_term thy
369dfc819056 unfold set constants in Sledgehammer/ATP as well if Metis does it too
blanchet
parents: 42734
diff changeset
   441
                     (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
   442
              |> 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
   443
              |> presimp ? presimplify_term ctxt
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   444
              |> perhaps (try (HOLogic.dest_Trueprop))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   445
              |> introduce_combinators_in_term ctxt kind
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   446
              |> kind <> Axiom ? freeze_term
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   447
    val (combformula, atomic_types) = combformula_from_prop thy eq_as_iff t []
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   448
  in
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   449
    {name = name, locality = loc, kind = kind, combformula = combformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   450
     atomic_types = atomic_types}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   451
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   452
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   453
fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, loc), t) =
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   454
  case (keep_trivial, make_formula ctxt eq_as_iff presimp name loc Axiom t) of
41990
7f2793d51efc add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents: 41770
diff changeset
   455
    (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
7f2793d51efc add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents: 41770
diff changeset
   456
    NONE
7f2793d51efc add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents: 41770
diff changeset
   457
  | (_, formula) => SOME formula
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   458
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   459
fun make_conjecture ctxt prem_kind ts =
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   460
  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
   461
    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
   462
             let
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   463
               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
   464
                 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
   465
                   (Conjecture, I)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   466
                 else
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   467
                   (prem_kind,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   468
                    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
   469
                    else I)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   470
              in
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   471
                make_formula ctxt true true (string_of_int j) Chained kind t
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   472
                |> maybe_negate
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   473
              end)
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   474
         (0 upto last) ts
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   475
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   476
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
   477
(** 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
   478
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
   479
(* 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
   480
   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
   481
   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
   482
   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
   483
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   484
fun should_encode_type _ (nonmono_Ts as _ :: _) _ T =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   485
    exists (curry Type.raw_instance T) nonmono_Ts
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   486
  | 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
   487
  | 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
   488
  | 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
   489
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   490
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
   491
                             should_predicate_on_var T =
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   492
     (heaviness = Heavy orelse should_predicate_on_var ()) andalso
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   493
     should_encode_type ctxt nonmono_Ts level T
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   494
  | 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
   495
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   496
fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   497
    String.isPrefix bound_var_prefix s
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   498
  | is_var_or_bound_var (CombVar _) = true
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   499
  | is_var_or_bound_var _ = false
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   500
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   501
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
   502
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   503
fun should_tag_with_type _ _ _ Top_Level _ _ = false
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   504
  | 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
   505
    (case heaviness of
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   506
       Heavy => should_encode_type ctxt nonmono_Ts level T
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   507
     | Light =>
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   508
       case (site, is_var_or_bound_var u) of
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   509
         (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
   510
       | _ => false)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   511
  | 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
   512
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
   513
val homo_infinite_T = @{typ ind} (* any infinite type *)
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
   514
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
   515
fun homogenized_type ctxt nonmono_Ts level 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
   516
  if should_encode_type ctxt nonmono_Ts level T then T else homo_infinite_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
   517
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
   518
(** "hBOOL" and "hAPP" **)
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   519
42574
blanchet
parents: 42573
diff changeset
   520
type sym_info =
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   521
  {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option}
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   522
42574
blanchet
parents: 42573
diff changeset
   523
fun add_combterm_syms_to_table 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
   524
  let
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
   525
    fun aux top_level tm =
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
   526
      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
   527
        (case head of
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   528
           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
   529
           if String.isPrefix bound_var_prefix s then
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
   530
             I
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
   531
           else
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   532
             let val ary = length args in
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
   533
               Symtab.map_default
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
   534
                   (s, {pred_sym = true,
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   535
                        min_ary = if explicit_apply then 0 else ary,
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   536
                        max_ary = 0, typ = SOME T})
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   537
                   (fn {pred_sym, min_ary, max_ary, typ} =>
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
   538
                       {pred_sym = pred_sym andalso top_level,
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   539
                        min_ary = Int.min (ary, min_ary),
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   540
                        max_ary = Int.max (ary, max_ary),
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   541
                        typ = if typ = SOME T then typ else NONE})
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
   542
            end
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
   543
         | _ => I)
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
   544
        #> fold (aux false) args
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
   545
      end
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
   546
  in aux true end
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   547
fun add_fact_syms_to_table explicit_apply =
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   548
  fact_lift (formula_fold NONE (K (add_combterm_syms_to_table explicit_apply)))
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   549
42675
223153bb68a1 added type annotation for SML/NJ
blanchet
parents: 42674
diff changeset
   550
val default_sym_table_entries : (string * sym_info) list =
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   551
  [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   552
   (make_fixed_const predicator_base,
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   553
    {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   554
  ([tptp_false, tptp_true]
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   555
   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   556
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   557
fun sym_table_for_facts explicit_apply facts =
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   558
  Symtab.empty |> fold Symtab.default default_sym_table_entries
42574
blanchet
parents: 42573
diff changeset
   559
               |> fold (add_fact_syms_to_table explicit_apply) facts
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   560
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
   561
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
   562
  case Symtab.lookup sym_tab s of
42574
blanchet
parents: 42573
diff changeset
   563
    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
   564
  | 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
   565
    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
   566
      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
   567
      let val s = s |> unmangled_const_name |> invert_const in
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   568
        if s = predicator_base then 1
42547
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
   569
        else if s = explicit_app_base then 2
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
   570
        else if s = type_pred_base then 1
42557
ae0deb39a254 fixed min-arity computation when "explicit_apply" is specified
blanchet
parents: 42556
diff changeset
   571
        else 0
42547
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
   572
      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
   573
    | NONE => 0
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   574
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   575
(* 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
   576
   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
   577
   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
   578
   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
   579
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
   580
  case Symtab.lookup sym_tab s of
42574
blanchet
parents: 42573
diff changeset
   581
    SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
blanchet
parents: 42573
diff changeset
   582
    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
   583
  | NONE => false
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   584
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   585
val predicator_combconst =
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   586
  CombConst (`make_fixed_const predicator_base, @{typ "bool => bool"}, [])
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   587
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
   588
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   589
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
   590
  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
   591
    (CombConst ((s, _), _, _), _) =>
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   592
    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
   593
  | _ => 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
   594
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   595
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
   596
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   597
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
   598
  let
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   599
    val head_T = combtyp_of head
42693
3c2baf9b3c61 reverted 6efda6167e5d because unsound -- Vampire found a counterexample
blanchet
parents: 42691
diff changeset
   600
    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
   601
    val explicit_app =
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   602
      CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
42693
3c2baf9b3c61 reverted 6efda6167e5d because unsound -- Vampire found a counterexample
blanchet
parents: 42691
diff changeset
   603
                 [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
   604
  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
   605
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
   606
42565
93f58e6a6f3e proper handling of partially applied proxy symbols
blanchet
parents: 42564
diff changeset
   607
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
   608
  let
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   609
    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
   610
      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
   611
        (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
   612
        args |> map aux
42557
ae0deb39a254 fixed min-arity computation when "explicit_apply" is specified
blanchet
parents: 42556
diff changeset
   613
             |> 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
   614
             |>> 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
   615
             |-> 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
   616
      | (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
   617
  in aux end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   618
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
   619
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
   620
  | 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
   621
    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
   622
  | 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
   623
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
   624
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
   625
  | 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
   626
    let
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   627
      (* will throw "TYPE" for pseudo-constants *)
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   628
      val U = if s = explicit_app_base then
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   629
                @{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
   630
              else
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   631
                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
   632
    in
42781
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   633
      case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   634
        [] => []
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   635
      | res_U_vars =>
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   636
        let val U_args = (s, U) |> Sign.const_typargs thy in
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   637
          U_args ~~ T_args
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   638
          |> map_filter (fn (U, T) =>
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   639
                            if member (op =) res_U_vars (dest_TVar U) then
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   640
                              SOME T
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   641
                            else
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   642
                              NONE)
4b7a988a0213 optimized a common case
blanchet
parents: 42780
diff changeset
   643
        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
   644
    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
   645
    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
   646
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
   647
fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
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
   648
  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
   649
    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
   650
    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
   651
        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
   652
      | 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
   653
        let
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   654
          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
   655
          val (T, T_args) =
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   656
            (* 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
   657
               anyway, by distinguishing overloads only on the homogenized
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   658
               result type. Don't do it for lightweight type systems, though,
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   659
               since it leads to too many unsound proofs. *)
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   660
            if s = const_prefix ^ explicit_app_base 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
   661
               length T_args = 2 andalso
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   662
               not (is_type_sys_virtually_sound type_sys) andalso
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   663
               heaviness_of_type_sys type_sys = Heavy then
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   664
              T_args |> map (homogenized_type ctxt nonmono_Ts level)
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   665
                     |> (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
   666
                                    (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
   667
                                  end)
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   668
            else
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   669
              (T, T_args)
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   670
        in
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   671
          (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
   672
             NONE => (name, T_args)
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   673
           | 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
   674
             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
   675
               val s'' = invert_const s''
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   676
               fun filtered_T_args false = T_args
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   677
                 | 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
   678
             in
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   679
               case type_arg_policy type_sys s'' of
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   680
                 Explicit_Type_Args drop_args =>
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   681
                 (name, filtered_T_args drop_args)
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   682
               | Mangled_Type_Args drop_args =>
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   683
                 (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
   684
               | 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
   685
             end)
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   686
          |> (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
   687
        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
   688
      | 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
   689
  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
   690
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   691
fun repair_combterm ctxt nonmono_Ts type_sys sym_tab =
42565
93f58e6a6f3e proper handling of partially applied proxy symbols
blanchet
parents: 42564
diff changeset
   692
  introduce_explicit_apps_in_combterm sym_tab
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   693
  #> introduce_predicators_in_combterm sym_tab
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
   694
  #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   695
fun repair_fact ctxt nonmono_Ts type_sys sym_tab =
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   696
  update_combformula (formula_map
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   697
      (repair_combterm ctxt 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
   698
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
   699
(** 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
   700
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
   701
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
   702
  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
   703
    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
   704
    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
   705
  in
42612
bb9143d7e217 cosmetics
blanchet
parents: 42608
diff changeset
   706
    Formula (helper_prefix ^ "ti_ti", 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
   707
             AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
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
   708
             |> 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
   709
  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
   710
42574
blanchet
parents: 42573
diff changeset
   711
fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : 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
   712
  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
   713
    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
   714
    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
   715
      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
   716
      val unmangled_s = mangled_s |> unmangled_const_name
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   717
      fun dub_and_inst c needs_some_types (th, j) =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   718
        ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   719
          Chained),
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
   720
         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
   721
           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
   722
                    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
   723
                  | _ => 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
   724
                 not (null (Term.hidden_polymorphism 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
   725
                ? (case typ 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
   726
                     SOME T => specialize_type thy (invert_const unmangled_s, 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
   727
                   | NONE => I)
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
   728
         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
   729
      fun make_facts eq_as_iff =
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
   730
        map_filter (make_fact ctxt false eq_as_iff false)
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
   731
      val has_some_types = 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
   732
    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
   733
      metis_helpers
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   734
      |> maps (fn (metis_s, (needs_some_types, 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
   735
                  if metis_s <> unmangled_s orelse
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
   736
                     (needs_some_types andalso not has_some_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
   737
                    []
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
   738
                  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
   739
                    ths ~~ (1 upto length ths)
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   740
                    |> map (dub_and_inst mangled_s needs_some_types)
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   741
                    |> make_facts (not needs_some_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
   742
    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
   743
  | 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
   744
fun helper_facts_for_sym_table ctxt type_sys sym_tab =
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
   745
  Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab []
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
   746
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
   747
fun translate_atp_fact ctxt keep_trivial =
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
   748
  `(make_fact ctxt keep_trivial true true o apsnd prop_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
   749
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   750
fun translate_formulas ctxt prem_kind type_sys hyp_ts concl_t 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
   751
  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
   752
    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
   753
    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
   754
    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
   755
      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
   756
      |> 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
   757
                      | (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
   758
      |> 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
   759
    (* 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
   760
       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
   761
    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
   762
    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
   763
    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
   764
    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
   765
    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
   766
    val tycons = type_consts_of_terms thy all_ts
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   767
    val conjs = make_conjecture ctxt prem_kind (hyp_ts @ [concl_t])
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
   768
    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
   769
      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
   770
      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
   771
    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
   772
  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
   773
    (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
   774
  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
   775
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
   776
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
   777
    (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
   778
  | 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
   779
    (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
   780
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
   781
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
   782
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
   783
fun type_pred_combatom ctxt nonmono_Ts type_sys T tm =
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   784
  CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T])
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   785
           |> 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
   786
           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
   787
  |> AAtom
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
   788
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   789
fun var_occurs_naked_in_term name (ATerm ((s, _), tms)) accum =
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   790
  accum orelse
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   791
  (s = "equal" andalso member (op =) tms (ATerm (name, [])))
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   792
fun var_occurs_naked_in_formula phi name =
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   793
  formula_fold NONE (K (var_occurs_naked_in_term name)) phi false
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   794
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   795
fun tag_with_type ctxt nonmono_Ts type_sys T tm =
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   796
  CombConst (`make_fixed_const type_tag_name, T --> T, [T])
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   797
  |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   798
  |> term_from_combterm ctxt nonmono_Ts type_sys Top_Level
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   799
  |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   800
and term_from_combterm ctxt nonmono_Ts type_sys site u =
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
   801
  let
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   802
    val (head, args) = strip_combterm_comb u
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   803
    val (x as (s, _), T_args) =
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   804
      case head of
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   805
        CombConst (name, _, T_args) => (name, T_args)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   806
      | CombVar (name, _) => (name, [])
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   807
      | CombApp _ => raise Fail "impossible \"CombApp\""
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   808
    val arg_site = if site = Top_Level andalso s = "equal" then Eq_Arg
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   809
                   else Elsewhere
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   810
    val t = ATerm (x, map fo_term_from_typ T_args @
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   811
                      map (term_from_combterm ctxt nonmono_Ts type_sys arg_site)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   812
                          args)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   813
    val T = combtyp_of u
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   814
  in
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   815
    t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   816
            tag_with_type ctxt nonmono_Ts type_sys T
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   817
          else
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   818
            I)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   819
  end
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   820
and formula_from_combformula ctxt nonmono_Ts type_sys should_predicate_on_var =
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   821
  let
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
   822
    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
   823
      case type_sys of
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   824
        Simple_Types level =>
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
   825
        SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
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
   826
      | _ => K NONE
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   827
    fun do_out_of_bound_type phi (name, T) =
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   828
      if should_predicate_on_type ctxt nonmono_Ts type_sys
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   829
             (fn () => should_predicate_on_var phi name) T then
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   830
        CombVar (name, T)
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   831
        |> type_pred_combatom ctxt nonmono_Ts type_sys T
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
   832
        |> do_formula |> SOME
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
   833
      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
   834
        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
   835
    and do_formula (AQuant (q, xs, phi)) =
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   836
        let val phi = phi |> do_formula in
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   837
          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
   838
                                        | 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
   839
                  (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
   840
                      (map_filter
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   841
                           (fn (_, NONE) => NONE
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   842
                             | (s, SOME T) =>
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   843
                               do_out_of_bound_type phi (s, T)) xs)
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   844
                      phi)
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   845
        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
   846
      | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   847
      | do_formula (AAtom tm) =
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   848
        AAtom (term_from_combterm ctxt nonmono_Ts type_sys Top_Level 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
   849
  in do_formula 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
   850
42727
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   851
fun bound_atomic_types type_sys Ts =
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   852
  mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   853
                (atp_type_literals_for_types type_sys Axiom Ts))
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   854
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   855
fun formula_for_fact 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
   856
                     ({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
   857
  combformula
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   858
  |> close_combformula_universally
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   859
  |> formula_from_combformula ctxt nonmono_Ts type_sys
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   860
                              var_occurs_naked_in_formula
42727
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
   861
  |> bound_atomic_types 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
   862
  |> 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
   863
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   864
fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   865
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
   866
(* 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
   867
   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
   868
   the remote provers might care. *)
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   869
fun formula_line_for_fact ctxt prefix nonmono_Ts type_sys
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   870
                          (j, formula as {name, locality, kind, ...}) =
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   871
  Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   872
                     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
   873
           ascii_of name,
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   874
           kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE,
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   875
           if generate_useful_info then
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   876
             case locality of
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   877
               Intro => useful_isabelle_info "intro"
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   878
             | Elim => useful_isabelle_info "elim"
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   879
             | Simp => useful_isabelle_info "simp"
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   880
             | _ => NONE
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   881
           else
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   882
             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
   883
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
fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
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
                                                       superclass, ...}) =
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
  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
   887
    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
   888
             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
   889
                               AAtom (ATerm (superclass, [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
   890
             |> 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
   891
  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
   892
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
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
   894
    (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
   895
  | 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
   896
    (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
   897
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
   898
fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
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
   899
                                                ...}) =
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
   900
  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
   901
           mk_ahorn (map (formula_from_fo_literal o apfst not
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
   902
                          o fo_literal_from_arity_literal) premLits)
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
   903
                    (formula_from_fo_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
   904
                         (fo_literal_from_arity_literal conclLit))
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
   905
           |> 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
   906
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   907
fun formula_line_for_conjecture 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
   908
        ({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
   909
  Formula (conjecture_prefix ^ name, kind,
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   910
           formula_from_combformula ctxt nonmono_Ts type_sys
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   911
                                    var_occurs_naked_in_formula
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
   912
                                    (close_combformula_universally combformula)
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
   913
           |> 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
   914
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
   915
fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
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
   916
  atomic_types |> atp_type_literals_for_types type_sys Conjecture
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
   917
               |> 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
   918
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
   919
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
   920
  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
   921
           formula_from_fo_literal lit, 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
   922
fun formula_lines_for_free_types type_sys 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
   923
  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
   924
    val litss = map (free_type_literals type_sys) 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
   925
    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
   926
  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
   927
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
   928
(** 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
   929
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
   930
fun insert_type get_T x xs =
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   931
  let val T = get_T x in
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   932
    if exists (curry Type.raw_instance T o get_T) xs then xs
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   933
    else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   934
  end
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   935
42574
blanchet
parents: 42573
diff changeset
   936
fun should_declare_sym type_sys pred_sym s =
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
   937
  not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
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
   938
  not (String.isPrefix tptp_special_prefix s) andalso
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   939
  ((case type_sys of
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   940
      Simple_Types _ => true
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   941
    | Tags (_, _, Light) => true
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   942
    | _ => false) orelse not pred_sym)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   943
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
   944
fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
42574
blanchet
parents: 42573
diff changeset
   945
  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
   946
    fun add_combterm in_conj tm =
42574
blanchet
parents: 42573
diff changeset
   947
      let val (head, args) = strip_combterm_comb tm in
blanchet
parents: 42573
diff changeset
   948
        (case head of
blanchet
parents: 42573
diff changeset
   949
           CombConst ((s, s'), T, T_args) =>
blanchet
parents: 42573
diff changeset
   950
           let val pred_sym = is_pred_sym repaired_sym_tab s in
blanchet
parents: 42573
diff changeset
   951
             if should_declare_sym type_sys pred_sym s then
42576
a8a80a2a34be merge symbol declarations that are type-instances of each other -- useful for type system "Args true" with monomorphization turned off
blanchet
parents: 42575
diff changeset
   952
               Symtab.map_default (s, [])
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
   953
                   (insert_type #3 (s', T_args, T, pred_sym, length args,
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
   954
                                    in_conj))
42574
blanchet
parents: 42573
diff changeset
   955
             else
blanchet
parents: 42573
diff changeset
   956
               I
blanchet
parents: 42573
diff changeset
   957
           end
blanchet
parents: 42573
diff changeset
   958
         | _ => I)
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
   959
        #> fold (add_combterm in_conj) args
42574
blanchet
parents: 42573
diff changeset
   960
      end
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
   961
    fun add_fact in_conj =
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   962
      fact_lift (formula_fold NONE (K (add_combterm in_conj)))
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
   963
  in
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
   964
    Symtab.empty
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
   965
    |> is_type_sys_fairly_sound type_sys
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
   966
       ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
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
   967
  end
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   968
42685
7a5116bd63b7 documentation tuning
blanchet
parents: 42684
diff changeset
   969
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
7a5116bd63b7 documentation tuning
blanchet
parents: 42684
diff changeset
   970
   out with monotonicity" paper presented at CADE 2011. *)
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   971
fun add_combterm_nonmonotonic_types _ _  (SOME false) _ = I
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   972
  | add_combterm_nonmonotonic_types ctxt level _
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   973
        (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   974
                  tm2)) =
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   975
    (exists is_var_or_bound_var [tm1, tm2] andalso
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   976
     (case level of
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   977
        Nonmonotonic_Types => not (is_type_surely_infinite ctxt T)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   978
      | Finite_Types => is_type_surely_finite ctxt T
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   979
      | _ => true)) ? insert_type I T
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   980
  | add_combterm_nonmonotonic_types _ _ _ _ = I
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   981
fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   982
                                            : translated_formula) =
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   983
  formula_fold (SOME (kind <> Conjecture))
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   984
               (add_combterm_nonmonotonic_types ctxt level) combformula
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   985
fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   986
  let val level = level_of_type_sys type_sys in
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   987
    (case level of
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   988
       Nonmonotonic_Types => true
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   989
     | Finite_Types =>
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   990
       heaviness_of_type_sys type_sys = Light andalso
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   991
       polymorphism_of_type_sys type_sys <> Polymorphic
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   992
     | _ => false)
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   993
    ? (fold (add_fact_nonmonotonic_types ctxt level) facts
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   994
       (* We must add bool in case the helper "True_or_False" is added later.
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   995
          In addition, several places in the code rely on the list of
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   996
          nonmonotonic types not being empty. *)
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   997
       #> insert_type I @{typ bool})
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
   998
  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
   999
42754
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1000
fun decl_line_for_sym ctxt nonmono_Ts level s (s', _, T, pred_sym, ary, _) =
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1001
  let
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1002
    val translate_type =
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1003
      mangled_type_name o homogenized_type ctxt nonmono_Ts level
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1004
    val (arg_tys, res_ty) =
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1005
      T |> chop_fun ary |>> map translate_type ||> translate_type
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1006
  in
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1007
    Decl (sym_decl_prefix ^ s, (s, s'), arg_tys,
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1008
          if pred_sym then `I tptp_tff_bool_type else res_ty)
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1009
  end
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1010
42592
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1011
fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1012
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1013
fun formula_line_for_pred_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s j
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1014
                                   (s', T_args, T, _, ary, in_conj) =
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1015
  let
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1016
    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
  1017
      if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1018
      else (Axiom, I)
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
  1019
    val (arg_Ts, res_T) = chop_fun ary T
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1020
    val bound_names =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1021
      1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1022
    val bounds =
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1023
      bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1024
    val bound_Ts =
42592
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1025
      arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1026
                             else NONE)
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1027
  in
42612
bb9143d7e217 cosmetics
blanchet
parents: 42608
diff changeset
  1028
    Formula (sym_decl_prefix ^ s ^
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1029
             (if n > 1 then "_" ^ string_of_int j else ""), kind,
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1030
             CombConst ((s, s'), T, T_args)
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1031
             |> fold (curry (CombApp o swap)) bounds
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
  1032
             |> type_pred_combatom ctxt nonmono_Ts type_sys res_T
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1033
             |> mk_aquant AForall (bound_names ~~ bound_Ts)
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1034
             |> formula_from_combformula ctxt nonmono_Ts type_sys (K (K true))
42727
f365f5138771 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents: 42726
diff changeset
  1035
             |> n > 1 ? bound_atomic_types type_sys (atyps_of T)
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1036
             |> close_formula_universally
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1037
             |> maybe_negate,
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1038
             NONE, NONE)
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1039
  end
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1040
42852
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1041
fun formula_lines_for_tag_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1042
                                  (j, (s', T_args, T, pred_sym, ary, in_conj)) =
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1043
  let
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1044
    val ident_base =
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1045
      sym_decl_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
42852
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1046
    val (kind, maybe_negate) =
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1047
      if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1048
      else (Axiom, I)
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1049
    val (arg_Ts, res_T) = chop_fun ary T
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1050
    val bound_names =
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1051
      1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1052
    val bounds = bound_names |> map (fn name => ATerm (name, []))
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1053
    fun const args = ATerm ((s, s'), map fo_term_from_typ T_args @ args)
42830
1068d8fc1331 generate type classes predicates in new "shallow" encoding
blanchet
parents: 42829
diff changeset
  1054
    val atomic_Ts = atyps_of T
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1055
    fun eq tms =
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1056
      (if pred_sym then AConn (AIff, map AAtom tms)
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1057
       else AAtom (ATerm (`I "equal", tms)))
42830
1068d8fc1331 generate type classes predicates in new "shallow" encoding
blanchet
parents: 42829
diff changeset
  1058
      |> bound_atomic_types type_sys atomic_Ts
1068d8fc1331 generate type classes predicates in new "shallow" encoding
blanchet
parents: 42829
diff changeset
  1059
      |> close_formula_universally
42852
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1060
      |> maybe_negate
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1061
    val should_encode = should_encode_type ctxt nonmono_Ts All_Types
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1062
    val tag_with = tag_with_type ctxt nonmono_Ts type_sys
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1063
    val add_formula_for_res =
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1064
      if should_encode res_T then
42852
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1065
        cons (Formula (ident_base ^ "_res", kind,
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1066
                       eq [tag_with res_T (const bounds), const bounds],
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1067
                       NONE, NONE))
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1068
      else
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1069
        I
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1070
    fun add_formula_for_arg k =
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1071
      let val arg_T = nth arg_Ts k in
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1072
        if should_encode arg_T then
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1073
          case chop k bounds of
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1074
            (bounds1, bound :: bounds2) =>
42852
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1075
            cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1076
                           eq [const (bounds1 @ tag_with arg_T bound ::
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1077
                                      bounds2),
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1078
                               const bounds],
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1079
                           NONE, NONE))
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1080
          | _ => raise Fail "expected nonempty tail"
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1081
        else
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1082
          I
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1083
      end
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1084
  in
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1085
    [] |> not pred_sym ? add_formula_for_res
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1086
       |> fold add_formula_for_arg (ary - 1 downto 0)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1087
  end
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1088
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1089
fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1090
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1091
fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1092
                                (s, decls) =
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
  1093
  case type_sys of
42754
b9d7df8c51c8 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
blanchet
parents: 42753
diff changeset
  1094
    Simple_Types level => map (decl_line_for_sym ctxt nonmono_Ts level s) decls
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1095
  | Preds _ =>
42574
blanchet
parents: 42573
diff changeset
  1096
    let
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1097
      val decls =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1098
        case decls of
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1099
          decl :: (decls' as _ :: _) =>
42592
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1100
          let val T = result_type_of_decl decl in
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1101
            if forall ((fn T' => Type.raw_instance (T', T))
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1102
                       o result_type_of_decl) decls' then
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1103
              [decl]
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1104
            else
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1105
              decls
fa2cf11d6351 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
blanchet
parents: 42589
diff changeset
  1106
          end
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1107
        | _ => decls
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1108
      val n = length decls
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1109
      val decls =
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1110
        decls
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1111
        |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1112
                   o result_type_of_decl)
42574
blanchet
parents: 42573
diff changeset
  1113
    in
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1114
      (0 upto length decls - 1, decls)
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1115
      |-> map2 (formula_line_for_pred_sym_decl ctxt conj_sym_kind nonmono_Ts
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1116
                                               type_sys n s)
42574
blanchet
parents: 42573
diff changeset
  1117
    end
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
  1118
  | Tags (_, _, heaviness) =>
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
  1119
    (case heaviness of
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
  1120
       Heavy => []
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
  1121
     | Light =>
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1122
       let val n = length decls in
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1123
         (0 upto n - 1 ~~ decls)
42852
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1124
         |> maps (formula_lines_for_tag_sym_decl ctxt conj_sym_kind nonmono_Ts
40649ab0cead honor "conj_sym_kind" also for tag symbol declarations
blanchet
parents: 42851
diff changeset
  1125
                                                 type_sys n s)
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1126
       end)
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1127
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1128
fun problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1129
                                     sym_decl_tab =
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1130
  Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt conj_sym_kind
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1131
                                                        nonmono_Ts type_sys)
42574
blanchet
parents: 42573
diff changeset
  1132
                  sym_decl_tab []
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1133
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1134
fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1135
    union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1136
  | add_tff_types_in_formula (AConn (_, phis)) =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1137
    fold add_tff_types_in_formula phis
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1138
  | add_tff_types_in_formula (AAtom _) = I
42539
f6ba908b8b27 generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents: 42538
diff changeset
  1139
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
  1140
fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
  1141
    union (op =) (res_T :: arg_Ts)
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
  1142
  | add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) =
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1143
    add_tff_types_in_formula phi
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1144
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1145
fun tff_types_in_problem problem =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1146
  fold (fold add_tff_types_in_problem_line o snd) problem []
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1147
42545
a14b602fb3d5 minor cleanup
blanchet
parents: 42544
diff changeset
  1148
fun decl_line_for_tff_type (s, s') =
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
  1149
  Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types)
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1150
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
  1151
fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
  1152
    level = Nonmonotonic_Types orelse level = Finite_Types
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
  1153
  | should_add_ti_ti_helper _ = false
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
  1154
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1155
val type_declsN = "Types"
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
  1156
val sym_declsN = "Symbol types"
41157
blanchet
parents: 41150
diff changeset
  1157
val factsN = "Relevant facts"
blanchet
parents: 41150
diff changeset
  1158
val class_relsN = "Class relationships"
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1159
val aritiesN = "Arities"
41157
blanchet
parents: 41150
diff changeset
  1160
val helpersN = "Helper facts"
blanchet
parents: 41150
diff changeset
  1161
val conjsN = "Conjectures"
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1162
val free_typesN = "Type variables"
41157
blanchet
parents: 41150
diff changeset
  1163
blanchet
parents: 41150
diff changeset
  1164
fun offset_of_heading_in_problem _ [] j = j
blanchet
parents: 41150
diff changeset
  1165
  | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
blanchet
parents: 41150
diff changeset
  1166
    if heading = needle then j
blanchet
parents: 41150
diff changeset
  1167
    else offset_of_heading_in_problem needle problem (j + length lines)
blanchet
parents: 41150
diff changeset
  1168
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1169
fun prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys explicit_apply
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1170
                        hyp_ts concl_t facts =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1171
  let
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1172
    val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1173
      translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
  1174
    val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
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
  1175
    val nonmono_Ts =
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
  1176
      [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
42701
500e4a88675e reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents: 42700
diff changeset
  1177
    val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab
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
  1178
    val (conjs, facts) = (conjs, facts) |> pairself (map repair)
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1179
    val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
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
  1180
    val helpers =
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
  1181
      repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1182
    val sym_decl_lines =
42731
2490e5e2f3f5 gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers
blanchet
parents: 42730
diff changeset
  1183
      (conjs, helpers @ facts)
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1184
      |> sym_decl_table_for_facts type_sys repaired_sym_tab
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
  1185
      |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
  1186
    (* Reordering these might confuse the proof reconstruction code or the SPASS
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
  1187
       Flotter hack. *)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1188
    val problem =
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
  1189
      [(sym_declsN, sym_decl_lines),
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1190
       (factsN, map (formula_line_for_fact ctxt fact_prefix nonmono_Ts type_sys)
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41990
diff changeset
  1191
                    (0 upto length facts - 1 ~~ facts)),
42545
a14b602fb3d5 minor cleanup
blanchet
parents: 42544
diff changeset
  1192
       (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
a14b602fb3d5 minor cleanup
blanchet
parents: 42544
diff changeset
  1193
       (aritiesN, map formula_line_for_arity_clause arity_clauses),
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1194
       (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1195
                                             type_sys)
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
  1196
                      (0 upto length helpers - 1 ~~ helpers)
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
  1197
                  |> should_add_ti_ti_helper type_sys
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
  1198
                     ? cons (ti_ti_helper_fact ())),
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1199
       (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1200
                    conjs),
42545
a14b602fb3d5 minor cleanup
blanchet
parents: 42544
diff changeset
  1201
       (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1202
    val problem =
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
  1203
      problem
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
  1204
      |> (case type_sys of
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
  1205
            Simple_Types _ =>
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
  1206
            cons (type_declsN,
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
  1207
                  map decl_line_for_tff_type (tff_types_in_problem problem))
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
  1208
          | _ => I)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
  1209
    val (problem, pool) =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
  1210
      problem |> nice_atp_problem (Config.get ctxt readable_names)
42778
896aaab98563 make SML/NJ happy
blanchet
parents: 42761
diff changeset
  1211
    fun add_sym_arity (s, {min_ary, ...} : sym_info) =
42755
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42754
diff changeset
  1212
      if min_ary > 0 then
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42754
diff changeset
  1213
        case strip_prefix_and_unascii const_prefix s of
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42754
diff changeset
  1214
          SOME s => Symtab.insert (op =) (s, min_ary)
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42754
diff changeset
  1215
        | NONE => I
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42754
diff changeset
  1216
      else
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42754
diff changeset
  1217
        I
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1218
  in
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1219
    (problem,
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1220
     case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
42585
723b9d1e8ba5 fixed embarrassing bug where conjecture and fact offsets were swapped
blanchet
parents: 42579
diff changeset
  1221
     offset_of_heading_in_problem conjsN problem 0,
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
  1222
     offset_of_heading_in_problem factsN problem 0,
42755
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42754
diff changeset
  1223
     fact_names |> Vector.fromList,
4603154a3018 robustly detect how many type args were passed to the ATP, even if some of them were omitted
blanchet
parents: 42754
diff changeset
  1224
     Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1225
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1226
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1227
(* FUDGE *)
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1228
val conj_weight = 0.0
41770
a710e96583d5 adjust fudge factors
blanchet
parents: 41769
diff changeset
  1229
val hyp_weight = 0.1
a710e96583d5 adjust fudge factors
blanchet
parents: 41769
diff changeset
  1230
val fact_min_weight = 0.2
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1231
val fact_max_weight = 1.0
42608
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1232
val type_info_default_weight = 0.8
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1233
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1234
fun add_term_weights weight (ATerm (s, tms)) =
42734
4a1fc1816dbb don't give weights to built-in symbols
blanchet
parents: 42731
diff changeset
  1235
  (not (is_atp_variable s) andalso s <> "equal" andalso
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
  1236
   not (String.isPrefix tptp_special_prefix s)) ? Symtab.default (s, weight)
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1237
  #> fold (add_term_weights weight) tms
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
  1238
fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1239
    formula_fold NONE (K (add_term_weights weight)) phi
42528
a15f0db2bcaf added support for TFF type declarations
blanchet
parents: 42527
diff changeset
  1240
  | add_problem_line_weights _ _ = I
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1241
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1242
fun add_conjectures_weights [] = I
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1243
  | add_conjectures_weights conjs =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1244
    let val (hyps, conj) = split_last conjs in
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1245
      add_problem_line_weights conj_weight conj
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1246
      #> fold (add_problem_line_weights hyp_weight) hyps
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1247
    end
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1248
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1249
fun add_facts_weights facts =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1250
  let
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1251
    val num_facts = length facts
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1252
    fun weight_of j =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1253
      fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1254
                        / Real.fromInt num_facts
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1255
  in
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1256
    map weight_of (0 upto num_facts - 1) ~~ facts
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1257
    |> fold (uncurry add_problem_line_weights)
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1258
  end
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1259
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1260
(* Weights are from 0.0 (most important) to 1.0 (least important). *)
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1261
fun atp_problem_weights problem =
42608
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1262
  let val get = these o AList.lookup (op =) problem in
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1263
    Symtab.empty
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1264
    |> add_conjectures_weights (get free_typesN @ get conjsN)
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1265
    |> add_facts_weights (get factsN)
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1266
    |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1267
            [sym_declsN, class_relsN, aritiesN]
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1268
    |> Symtab.dest
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1269
    |> sort (prod_ord Real.compare string_ord o pairself swap)
6ef61823b63b make sure E type information constants are given a weight, even if they don't appear anywhere else
blanchet
parents: 42592
diff changeset
  1270
  end
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1271
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1272
end;