src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
author blanchet
Thu, 05 May 2011 00:22:37 +0200
changeset 42688 097a61baeca9
parent 42687 8a4682bf70ed
child 42689 e38590764c34
permissions -rw-r--r--
smoother handling of ! and ? in type system names
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
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    12
  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
    13
  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
    14
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
  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
    16
  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
    17
    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_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
    18
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    19
  datatype type_system =
42684
2123b2608b14 renamed "many_typed" to "simple" (as in simple types)
blanchet
parents: 42682
diff changeset
    20
    Simple of type_level |
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    21
    Preds of polymorphism * 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
    22
    Tags of polymorphism * 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
    23
40114
blanchet
parents: 40069
diff changeset
    24
  type translated_formula
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    25
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
    26
  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
    27
  val fact_prefix : string
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    28
  val conjecture_prefix : string
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    29
  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
    30
  val explicit_app_base : string
42549
b9754f26c7bc handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents: 42548
diff changeset
    31
  val type_pred_base : string
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
    32
  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
    33
  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
    34
  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
    35
  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
    36
  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
    37
  val is_type_sys_fairly_sound : type_system -> bool
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
    38
  val num_atp_type_args : theory -> type_system -> string -> int
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
    39
  val unmangled_const : string -> string * string fo_term list
41088
54eb8e7c7f9b clarified terminology
blanchet
parents: 40204
diff changeset
    40
  val translate_atp_fact :
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    41
    Proof.context -> bool -> (string * locality) * thm
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    42
    -> translated_formula option * ((string * locality) * thm)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39975
diff changeset
    43
  val prepare_atp_problem :
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    44
    Proof.context -> type_system -> bool -> term list -> term
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
    45
    -> (translated_formula option * ((string * 'a) * thm)) list
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
    46
    -> string problem * string Symtab.table * int * int
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
    47
       * (string * 'a) list vector
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
    48
  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
    49
end;
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    50
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
    51
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
    52
struct
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    53
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    54
open ATP_Problem
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39452
diff changeset
    55
open Metis_Translate
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    56
open Sledgehammer_Util
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    57
open Sledgehammer_Filter
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    58
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    59
(* experimental *)
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
    60
val generate_useful_info = false
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    61
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    62
(* 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
    63
   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
    64
   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
    65
   readable. For these reason, they are enabled by default. *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
    66
val readable_names =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42645
diff changeset
    67
  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
    68
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    69
val type_decl_prefix = "type_"
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    70
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
    71
val fact_prefix = "fact_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    72
val conjecture_prefix = "conj_"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    73
val helper_prefix = "help_"
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    74
val class_rel_clause_prefix = "crel_";
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    75
val arity_clause_prefix = "arity_"
39975
7c50d5ca5c04 avoid generating several formulas with the same name ("tfrees")
blanchet
parents: 39954
diff changeset
    76
val tfree_prefix = "tfree_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    77
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    78
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
    79
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
    80
val type_pred_base = "is"
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
    81
val tff_type_prefix = "ty_"
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
    82
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
    83
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
    84
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    85
(* official TPTP syntax *)
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    86
val tptp_tff_type_of_types = "$tType"
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    87
val tptp_tff_bool_type = "$o"
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    88
val tptp_false = "$false"
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
    89
val tptp_true = "$true"
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
    90
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    91
(* Freshness almost guaranteed! *)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    92
val sledgehammer_weak_prefix = "Sledgehammer:"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    93
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
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
    95
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
    96
  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_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
    97
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
    98
datatype type_system =
42684
2123b2608b14 renamed "many_typed" to "simple" (as in simple types)
blanchet
parents: 42682
diff changeset
    99
  Simple of type_level |
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
   100
  Preds of polymorphism * 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
   101
  Tags of polymorphism * 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
   102
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 =
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
   104
  (case try (unprefix "mangled_") s of
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
   105
     SOME s => (Mangled_Monomorphic, 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
   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
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
   108
       SOME s => (Monomorphic, 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
   109
     | NONE => (Polymorphic, 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
   110
  ||> (fn s =>
42688
097a61baeca9 smoother handling of ! and ? in type system names
blanchet
parents: 42687
diff changeset
   111
          case try (unsuffix "?") 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
   112
            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
   113
          | NONE =>
42688
097a61baeca9 smoother handling of ! and ? in type system names
blanchet
parents: 42687
diff changeset
   114
            case try (unsuffix "!") 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
   115
              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
   116
            | NONE => (All_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
  |> (fn (polymorphism, (level, core)) =>
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
   118
         case (core, (polymorphism, level)) of
42684
2123b2608b14 renamed "many_typed" to "simple" (as in simple types)
blanchet
parents: 42682
diff changeset
   119
           ("simple", (Polymorphic (* naja *), level)) => Simple level
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
   120
         | ("preds", extra) => Preds extra
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   121
         | ("tags", extra) => Tags extra
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
   122
         | ("args", (_, All_Types (* naja *))) =>
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
   123
           Preds (polymorphism, Const_Arg_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
   124
         | ("erased", (Polymorphic, All_Types (* naja *))) =>
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   125
           Preds (polymorphism, No_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
   126
         | _ => error ("Unknown type system: " ^ quote 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
   127
42684
2123b2608b14 renamed "many_typed" to "simple" (as in simple types)
blanchet
parents: 42682
diff changeset
   128
fun polymorphism_of_type_sys (Simple _) = Mangled_Monomorphic
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
   129
  | polymorphism_of_type_sys (Preds (poly, _)) = poly
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
   130
  | polymorphism_of_type_sys (Tags (poly, _)) = poly
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
   131
42684
2123b2608b14 renamed "many_typed" to "simple" (as in simple types)
blanchet
parents: 42682
diff changeset
   132
fun level_of_type_sys (Simple level) = level
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
   133
  | level_of_type_sys (Preds (_, level)) = 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
   134
  | level_of_type_sys (Tags (_, level)) = 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
   135
42687
blanchet
parents: 42685
diff changeset
   136
fun is_type_level_virtually_sound level =
blanchet
parents: 42685
diff changeset
   137
  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
   138
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
   139
  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
   140
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   141
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
   142
  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
   143
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
   144
42687
blanchet
parents: 42685
diff changeset
   145
fun is_type_level_partial level =
blanchet
parents: 42685
diff changeset
   146
  level = Nonmonotonic_Types orelse level = Finite_Types
blanchet
parents: 42685
diff changeset
   147
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
   148
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
   149
  | 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
   150
  | 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
   151
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   152
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
   153
  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
   154
    fun aux pos (AQuant (_, _, phi)) = aux pos phi
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   155
      | 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
   156
      | aux pos (AConn (AImplies, [phi1, phi2])) =
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   157
        aux (Option.map not pos) phi1 #> aux pos phi2
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   158
      | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   159
      | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   160
      | 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
   161
      | aux pos (AAtom tm) = f pos tm
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   162
  in aux (SOME 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
   163
40114
blanchet
parents: 40069
diff changeset
   164
type translated_formula =
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38748
diff changeset
   165
  {name: string,
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   166
   locality: locality,
42525
7a506b0b644f distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree
blanchet
parents: 42524
diff changeset
   167
   kind: formula_kind,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   168
   combformula: (name, typ, combterm) formula,
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   169
   atomic_types: typ list}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   170
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   171
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
   172
                          : translated_formula) =
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   173
  {name = name, locality = locality, kind = kind, combformula = f combformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   174
   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
   175
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
   176
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
   177
42572
0c9a947b43fc drop "fequal" type args for unmangled type systems
blanchet
parents: 42570
diff changeset
   178
val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
0c9a947b43fc drop "fequal" type args for unmangled type systems
blanchet
parents: 42570
diff changeset
   179
0c9a947b43fc drop "fequal" type args for unmangled type systems
blanchet
parents: 42570
diff changeset
   180
fun should_omit_type_args type_sys 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
   181
  s <> type_pred_base andalso s <> type_tag_name andalso
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
   182
  (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse
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
   183
   (case type_sys of
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
   184
      Tags (_, All_Types) => true
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
   185
    | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
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
   186
           member (op =) boring_consts s))
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
   187
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
   188
datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_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
   189
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
   190
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
   191
  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
   192
    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
   193
  else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic 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
   194
    Mangled_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
   195
  else
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
   196
    Explicit_Type_Args
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   197
42524
3df98f0de5a0 remove experimental feature ("risky overload")
blanchet
parents: 42523
diff changeset
   198
fun type_arg_policy type_sys s =
42572
0c9a947b43fc drop "fequal" type args for unmangled type systems
blanchet
parents: 42570
diff changeset
   199
  if should_omit_type_args type_sys s then No_Type_Args
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   200
  else 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
   201
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
   202
fun num_atp_type_args thy type_sys s =
42557
ae0deb39a254 fixed min-arity computation when "explicit_apply" is specified
blanchet
parents: 42556
diff changeset
   203
  if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
ae0deb39a254 fixed min-arity computation when "explicit_apply" is specified
blanchet
parents: 42556
diff changeset
   204
  else 0
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
   205
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
   206
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
   207
  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
   208
    []
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
   209
  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
   210
    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
   211
       |> 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
   212
                   | 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
   213
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   214
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
   215
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
   216
  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
   217
    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
   218
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   219
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
   220
  | 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
   221
fun mk_aquant _ [] phi = phi
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   222
  | 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
   223
    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
   224
  | 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
   225
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   226
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
   227
  let
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   228
    fun formula_vars bounds (AQuant (_, xs, phi)) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   229
        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
   230
      | 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
   231
      | formula_vars bounds (AAtom tm) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   232
        union (op =) (atom_vars tm []
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   233
                      |> 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
   234
  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
   235
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   236
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
   237
  | combterm_vars (CombConst _) = I
42574
blanchet
parents: 42573
diff changeset
   238
  | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   239
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
   240
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   241
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
   242
  is_atp_variable s ? insert (op =) (name, NONE)
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   243
  #> fold term_vars tms
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   244
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
   245
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   246
fun fo_term_from_typ (Type (s, Ts)) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   247
    ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts)
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   248
  | fo_term_from_typ (TFree (s, _)) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   249
    ATerm (`make_fixed_type_var s, [])
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   250
  | fo_term_from_typ (TVar ((x as (s, _)), _)) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   251
    ATerm ((make_schematic_type_var x, s), [])
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   252
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   253
(* 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
   254
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
   255
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   256
fun generic_mangled_type_name f (ATerm (name, [])) = f name
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   257
  | generic_mangled_type_name f (ATerm (name, tys)) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   258
    f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")"
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   259
val mangled_type_name =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   260
  fo_term_from_typ
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   261
  #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   262
                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
   263
42574
blanchet
parents: 42573
diff changeset
   264
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
   265
  fold_rev (curry (op ^) o g o prefix mangled_type_sep
42574
blanchet
parents: 42573
diff changeset
   266
            o generic_mangled_type_name f) Ts ""
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   267
fun mangled_const_name T_args (s, s') =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   268
  let val ty_args = map fo_term_from_typ T_args in
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   269
    (s ^ generic_mangled_type_suffix fst ascii_of ty_args,
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   270
     s' ^ generic_mangled_type_suffix snd I ty_args)
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   271
  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
   272
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
   273
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
   274
  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
   275
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
   276
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
   277
  (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
   278
   -- 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
   279
                    [] >> 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
   280
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
   281
  (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
   282
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
   283
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
   284
  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
   285
    |> 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
   286
           (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
   287
                                                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
   288
    |> 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
   289
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   290
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
   291
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
   292
  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
   293
    (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
   294
  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
   295
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   296
fun introduce_proxies tm =
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   297
  let
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   298
    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
   299
        CombApp (aux top_level tm1, aux false tm2)
42574
blanchet
parents: 42573
diff changeset
   300
      | 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
   301
        (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
   302
           SOME proxy_base =>
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   303
           if top_level then
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   304
             (case s of
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   305
                "c_False" => (tptp_false, s')
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   306
              | "c_True" => (tptp_true, s')
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   307
              | _ => name, [])
42569
5737947e4c77 make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents: 42568
diff changeset
   308
           else
42574
blanchet
parents: 42573
diff changeset
   309
             (proxy_base |>> prefix const_prefix, T_args)
blanchet
parents: 42573
diff changeset
   310
          | NONE => (name, T_args))
blanchet
parents: 42573
diff changeset
   311
        |> (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
   312
      | aux _ tm = tm
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   313
  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
   314
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   315
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
   316
  let
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   317
    fun do_term bs t atomic_types =
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   318
      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
   319
      |>> (introduce_proxies #> AAtom)
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   320
      ||> union (op =) atomic_types
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   321
    fun do_quant bs q s T t' =
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   322
      let val s = Name.variant (map fst bs) s in
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   323
        do_formula ((s, T) :: bs) t'
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   324
        #>> mk_aquant q [(`make_bound_var s, SOME T)]
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   325
      end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   326
    and do_conn bs c t1 t2 =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   327
      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
   328
      #>> uncurry (mk_aconn c)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   329
    and do_formula bs t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   330
      case t of
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   331
        @{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
   332
      | 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
   333
        do_quant bs AForall s T t'
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   334
      | 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
   335
        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
   336
      | @{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
   337
      | @{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
   338
      | @{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
   339
      | 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
   340
        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
   341
      | _ => do_term bs t
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   342
  in do_formula [] end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   343
38618
5536897d04c2 remove trivial facts
blanchet
parents: 38613
diff changeset
   344
val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   345
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41406
diff changeset
   346
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
   347
fun conceal_bounds Ts t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   348
  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
   349
                    (0 upto length Ts - 1 ~~ Ts), t)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   350
fun reveal_bounds Ts =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   351
  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
   352
                    (0 upto length Ts - 1 ~~ Ts))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   353
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
   354
(* Removes the lambdas from an equation of the form "t = (%x. u)".
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39886
diff changeset
   355
   (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
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
   356
fun extensionalize_term t =
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
   357
  let
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
   358
    fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
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
   359
      | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
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
   360
                                        Type (_, [_, res_T])]))
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
   361
                    $ t2 $ Abs (var_s, var_T, t')) =
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   362
        if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
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
   363
          let val var_t = Var ((var_s, j), var_T) in
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
   364
            Const (s, T' --> T' --> res_T)
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
   365
              $ betapply (t2, var_t) $ subst_bound (var_t, t')
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
   366
            |> aux (j + 1)
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
   367
          end
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
   368
        else
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
   369
          t
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
   370
      | aux _ t = t
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
   371
  in aux (maxidx_of_term t + 1) t end
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
   372
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   373
fun introduce_combinators_in_term ctxt kind t =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   374
  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
   375
    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
   376
      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
   377
    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
   378
      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
   379
        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
   380
          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
   381
            @{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
   382
          | (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
   383
            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
   384
          | (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
   385
            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
   386
          | (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
   387
            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
   388
          | (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
   389
            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
   390
          | (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
   391
          | (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
   392
          | (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
   393
          | (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
   394
              $ 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
   395
            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
   396
          | _ => 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
   397
                   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
   398
                 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
   399
                   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
   400
                     |> 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
   401
                     |> cterm_of thy
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39886
diff changeset
   402
                     |> 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
   403
                     |> 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
   404
                     |> reveal_bounds Ts
39370
f8292d3020db use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents: 39005
diff changeset
   405
        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
   406
      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
   407
      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
   408
             (* 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
   409
             if kind = Conjecture then HOLogic.false_const
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   410
             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
   411
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   412
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   413
(* 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
   414
   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
   415
fun freeze_term t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   416
  let
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   417
    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
   418
      | 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
   419
      | aux (Var ((s, i), T)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   420
        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
   421
      | aux t = t
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   422
  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
   423
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
   424
(* making fact and conjecture formulas *)
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   425
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
   426
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   427
    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
   428
    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
   429
              |> transform_elim_term
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41199
diff changeset
   430
              |> Object_Logic.atomize_term thy
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   431
    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
   432
    val t = t |> need_trueprop ? HOLogic.mk_Trueprop
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   433
              |> extensionalize_term
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   434
              |> presimp ? presimplify_term thy
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   435
              |> perhaps (try (HOLogic.dest_Trueprop))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   436
              |> introduce_combinators_in_term ctxt kind
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   437
              |> kind <> Axiom ? freeze_term
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   438
    val (combformula, atomic_types) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   439
      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
   440
  in
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   441
    {name = name, locality = loc, kind = kind, combformula = combformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   442
     atomic_types = atomic_types}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   443
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   444
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   445
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
   446
  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
   447
    (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
   448
    NONE
7f2793d51efc add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents: 41770
diff changeset
   449
  | (_, formula) => SOME formula
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   450
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   451
fun make_conjecture ctxt ts =
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   452
  let val last = length ts - 1 in
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   453
    map2 (fn j => make_formula ctxt true true (string_of_int j) Chained
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   454
                               (if j = last then Conjecture else Hypothesis))
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   455
         (0 upto last) ts
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   456
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   457
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
   458
(** 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
   459
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
   460
(* 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
   461
   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
   462
   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
   463
   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
   464
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
   465
fun datatype_constrs thy (T as Type (s, 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
   466
    (case Datatype.get_info thy s of
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
   467
       SOME {index, descr, ...} =>
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
   468
       let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
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
   469
         map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> 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
   470
             constrs
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
   471
       end
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
   472
     | NONE => [])
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
   473
  | datatype_constrs _ _ = []
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
   474
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
   475
(* Similar to "Nitpick_HOL.bounded_exact_card_of_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
   476
   0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
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
   cardinality 2 or more. The specified default cardinality is returned if the
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
   cardinality of the type can't be determined. *)
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
fun tiny_card_of_type ctxt default_card 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
   480
  let
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
    val max = 2 (* 1 would be too small for the "fun" case *)
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
    fun aux avoid 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
   483
      (if member (op =) avoid T then
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
   484
         0
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
   485
       else case T of
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
   486
         Type (@{type_name fun}, [T1, T2]) =>
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
         (case (aux avoid T1, aux avoid T2) of
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
            (_, 1) => 1
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
          | (0, _) => 0
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
   490
          | (_, 0) => 0
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
   491
          | (k1, k2) =>
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
   492
            if k1 >= max orelse k2 >= max then max
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
   493
            else Int.min (max, Integer.pow k2 k1))
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
   494
       | @{typ int} => 0
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
       | @{typ bool} => 2 (* optimization *)
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
   496
       | 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
   497
         let val thy = Proof_Context.theory_of ctxt in
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
   498
           case datatype_constrs thy T of
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
   499
             [] => default_card
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
   500
           | constrs =>
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
   501
             let
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
   502
               val constr_cards =
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
   503
                 map (Integer.prod o map (aux (T :: avoid)) o binder_types
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
   504
                      o snd) constrs
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
   505
             in
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
   506
               if exists (curry (op =) 0) constr_cards then 0
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
   507
               else Int.min (max, Integer.sum constr_cards)
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
   508
             end
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
   509
         end
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
   510
       | _ => default_card)
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
   511
  in Int.min (max, aux [] T) end
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
fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
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
fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
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
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
fun should_encode_type _ _ All_Types _ = true
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
  | 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
   518
  | should_encode_type _ nonmono_Ts Nonmonotonic_Types 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
   519
    exists (curry Type.raw_instance T) 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
   520
  | 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
   521
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
   522
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, 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
   523
    should_encode_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
   524
  | should_predicate_on_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
   525
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
   526
fun should_tag_with_type ctxt nonmono_Ts (Tags (_, 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
   527
    should_encode_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
   528
  | should_tag_with_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
   529
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   530
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
   531
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   532
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
   533
  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
   534
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
   535
(** "hBOOL" and "hAPP" **)
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   536
42574
blanchet
parents: 42573
diff changeset
   537
type sym_info =
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   538
  {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option}
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   539
42574
blanchet
parents: 42573
diff changeset
   540
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
   541
  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
   542
    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
   543
      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
   544
        (case head of
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   545
           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
   546
           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
   547
             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
   548
           else
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   549
             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
   550
               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
   551
                   (s, {pred_sym = true,
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   552
                        min_ary = if explicit_apply then 0 else ary,
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   553
                        max_ary = 0, typ = SOME T})
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   554
                   (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
   555
                       {pred_sym = pred_sym andalso top_level,
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   556
                        min_ary = Int.min (ary, min_ary),
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   557
                        max_ary = Int.max (ary, max_ary),
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   558
                        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
   559
            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
   560
         | _ => 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
   561
        #> 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
   562
      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
   563
  in aux true end
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   564
fun add_fact_syms_to_table explicit_apply =
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   565
  fact_lift (formula_fold true (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
   566
42675
223153bb68a1 added type annotation for SML/NJ
blanchet
parents: 42674
diff changeset
   567
val default_sym_table_entries : (string * sym_info) list =
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   568
  [("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
   569
   (make_fixed_const predicator_base,
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   570
    {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
   571
  ([tptp_false, tptp_true]
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   572
   |> 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
   573
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   574
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
   575
  Symtab.empty |> fold Symtab.default default_sym_table_entries
42574
blanchet
parents: 42573
diff changeset
   576
               |> 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
   577
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   578
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
   579
  case Symtab.lookup sym_tab s of
42574
blanchet
parents: 42573
diff changeset
   580
    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
   581
  | 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
   582
    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
   583
      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
   584
      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
   585
        if s = predicator_base then 1
42547
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
   586
        else if s = explicit_app_base then 2
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
   587
        else if s = type_pred_base then 1
42557
ae0deb39a254 fixed min-arity computation when "explicit_apply" is specified
blanchet
parents: 42556
diff changeset
   588
        else 0
42547
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
   589
      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
   590
    | NONE => 0
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   591
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   592
(* 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
   593
   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
   594
   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
   595
   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
   596
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
   597
  case Symtab.lookup sym_tab s of
42574
blanchet
parents: 42573
diff changeset
   598
    SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
blanchet
parents: 42573
diff changeset
   599
    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
   600
  | NONE => false
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   601
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   602
val predicator_combconst =
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   603
  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
   604
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
   605
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   606
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
   607
  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
   608
    (CombConst ((s, _), _, _), _) =>
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   609
    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
   610
  | _ => 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
   611
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   612
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
   613
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   614
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
   615
  let
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   616
    val head_T = combtyp_of head
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   617
    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
   618
    val explicit_app =
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   619
      CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   620
                 [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
   621
  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
   622
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
   623
42565
93f58e6a6f3e proper handling of partially applied proxy symbols
blanchet
parents: 42564
diff changeset
   624
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
   625
  let
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   626
    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
   627
      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
   628
        (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
   629
        args |> map aux
42557
ae0deb39a254 fixed min-arity computation when "explicit_apply" is specified
blanchet
parents: 42556
diff changeset
   630
             |> 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
   631
             |>> 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
   632
             |-> 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
   633
      | (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
   634
  in aux end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   635
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
   636
fun impose_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
   637
  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
   638
    fun aux (CombApp tmp) = CombApp (pairself aux tmp)
42574
blanchet
parents: 42573
diff changeset
   639
      | aux (CombConst (name as (s, _), T, T_args)) =
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
   640
        let
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
   641
          val level = level_of_type_sys type_sys
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
   642
          val (T, T_args) =
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
   643
            (* avoid needless identical homogenized versions of "hAPP" *)
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
   644
            if s = const_prefix ^ explicit_app_base then
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
   645
              T_args |> map (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
   646
                     |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
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
   647
                                    (T --> T, 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
   648
                                  end)
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
   649
            else
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
   650
              (T, T_args)
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
   651
        in
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
   652
          (case strip_prefix_and_unascii const_prefix s of
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
   653
             NONE => (name, T_args)
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
   654
           | SOME s'' =>
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
   655
             let val s'' = invert_const s'' in
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
   656
               case type_arg_policy type_sys s'' of
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
   657
                 No_Type_Args => (name, [])
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
   658
               | Explicit_Type_Args => (name, T_args)
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
   659
               | Mangled_Type_Args => (mangled_const_name T_args name, [])
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
   660
             end)
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
   661
          |> (fn (name, T_args) => CombConst (name, T, T_args))
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
   662
        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
   663
      | aux tm = 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
   664
  in aux 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
   665
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
   666
fun repair_combterm ctxt nonmono_Ts type_sys sym_tab =
42565
93f58e6a6f3e proper handling of partially applied proxy symbols
blanchet
parents: 42564
diff changeset
   667
  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
   668
  #> introduce_predicators_in_combterm 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
   669
  #> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
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
   670
fun repair_fact ctxt nonmono_Ts type_sys sym_tab =
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
   671
  update_combformula (formula_map
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
   672
      (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
   673
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
   674
(** 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
   675
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
   676
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
   677
  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
   678
    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
   679
    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
   680
  in
42612
bb9143d7e217 cosmetics
blanchet
parents: 42608
diff changeset
   681
    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
   682
             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
   683
             |> 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
   684
  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
   685
42574
blanchet
parents: 42573
diff changeset
   686
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
   687
  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
   688
    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
   689
    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
   690
      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
   691
      val unmangled_s = mangled_s |> unmangled_const_name
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   692
      fun dub_and_inst c needs_some_types (th, j) =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   693
        ((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
   694
          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
   695
         let val t = th |> prop_of 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
   696
           t |> (general_type_arg_policy type_sys = Mangled_Type_Args 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
   697
                 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
   698
                ? (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
   699
                     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
   700
                   | 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
   701
         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
   702
      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
   703
        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
   704
      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
   705
    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
   706
      metis_helpers
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   707
      |> 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
   708
                  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
   709
                     (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
   710
                    []
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
   711
                  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
   712
                    ths ~~ (1 upto length ths)
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   713
                    |> map (dub_and_inst mangled_s needs_some_types)
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   714
                    |> 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
   715
    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
   716
  | 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
   717
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
   718
  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
   719
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
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
   721
  `(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
   722
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
   723
fun translate_formulas ctxt type_sys hyp_ts concl_t 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
   724
  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
   725
    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
   726
    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
   727
    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
   728
      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
   729
      |> 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
   730
                      | (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
   731
      |> 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
   732
    (* 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
   733
       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
   734
    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
   735
    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
   736
    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
   737
    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
   738
    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
   739
    val tycons = type_consts_of_terms thy 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
   740
    val conjs = make_conjecture ctxt (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
   741
    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
   742
      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
   743
      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
   744
    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
   745
  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
   746
    (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
   747
  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
   748
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
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
   750
    (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
   751
  | 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
   752
    (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
   753
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
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
   755
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
   756
fun type_pred_combatom ctxt nonmono_Ts type_sys T 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
   757
  CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [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
   758
           tm)
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
   759
  |> impose_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
   760
  |> 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
   761
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   762
fun formula_from_combformula 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
   763
  let
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
   764
    fun tag_with_type type_sys T tm =
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
   765
      CombConst (`make_fixed_const type_tag_name, T --> T, [T])
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
   766
      |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts 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
   767
      |> do_term true
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
   768
      |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
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
    and do_term top_level 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
   770
      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
   771
        val (head, args) = strip_combterm_comb u
42574
blanchet
parents: 42573
diff changeset
   772
        val (x, T_args) =
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
   773
          case head of
42574
blanchet
parents: 42573
diff changeset
   774
            CombConst (name, _, T_args) => (name, T_args)
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
   775
          | CombVar (name, _) => (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
   776
          | CombApp _ => raise Fail "impossible \"CombApp\""
42574
blanchet
parents: 42573
diff changeset
   777
        val t = ATerm (x, map fo_term_from_typ T_args @
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
   778
                          map (do_term false) args)
42574
blanchet
parents: 42573
diff changeset
   779
        val T = combtyp_of 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
   780
      in
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   781
        t |> (if not top_level andalso
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   782
                should_tag_with_type ctxt nonmono_Ts type_sys T then
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
   783
                tag_with_type 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
   784
              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
   785
                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
   786
      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
   787
    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
   788
      case type_sys of
42684
2123b2608b14 renamed "many_typed" to "simple" (as in simple types)
blanchet
parents: 42682
diff changeset
   789
        Simple 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
   790
        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
   791
      | _ => K 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
   792
    fun do_out_of_bound_type (s, T) =
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   793
      if should_predicate_on_type ctxt nonmono_Ts type_sys T then
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
   794
        type_pred_combatom ctxt nonmono_Ts type_sys T (CombVar (s, 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
   795
        |> 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
   796
      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
   797
        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
   798
    and do_formula (AQuant (q, xs, 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
   799
        AQuant (q, xs |> map (apsnd (fn NONE => NONE
42574
blanchet
parents: 42573
diff changeset
   800
                                      | SOME T => do_bound_type 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
   801
                (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   802
                    (map_filter
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   803
                         (fn (_, NONE) => NONE
42574
blanchet
parents: 42573
diff changeset
   804
                           | (s, SOME T) => do_out_of_bound_type (s, T)) xs)
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
   805
                    (do_formula 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
   806
      | do_formula (AConn (c, phis)) = AConn (c, map do_formula 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
   807
      | do_formula (AAtom tm) = AAtom (do_term true 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
   808
  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
   809
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   810
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
   811
                     ({combformula, 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
   812
  mk_ahorn (map (formula_from_fo_literal o 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
   813
                (atp_type_literals_for_types type_sys Axiom atomic_types))
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   814
           (formula_from_combformula 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
   815
                (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
   816
  |> 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
   817
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   818
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
   819
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
   820
(* 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
   821
   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
   822
   the remote provers might care. *)
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   823
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
   824
                          (j, formula as {name, locality, kind, ...}) =
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   825
  Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   826
                     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
   827
           ascii_of name,
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   828
           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
   829
           if generate_useful_info then
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   830
             case locality of
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   831
               Intro => useful_isabelle_info "intro"
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   832
             | Elim => useful_isabelle_info "elim"
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   833
             | Simp => useful_isabelle_info "simp"
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   834
             | _ => NONE
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   835
           else
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   836
             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
   837
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   838
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
   839
                                                       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
   840
  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
   841
    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
   842
             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
   843
                               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
   844
             |> 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
   845
  end
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   846
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
   847
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
   848
    (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
   849
  | 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
   850
    (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
   851
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
   852
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
   853
                                                ...}) =
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
   854
  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
   855
           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
   856
                          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
   857
                    (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
   858
                         (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
   859
           |> 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
   860
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   861
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
   862
        ({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
   863
  Formula (conjecture_prefix ^ name, kind,
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   864
           formula_from_combformula 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
   865
                                    (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
   866
           |> 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
   867
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
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
   869
  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
   870
               |> 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
   871
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
   872
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
   873
  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
   874
           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
   875
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
   876
  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
   877
    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
   878
    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
   879
  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
   880
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
   881
(** 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
   882
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
   883
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
   884
  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
   885
    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
   886
    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
   887
  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
   888
42574
blanchet
parents: 42573
diff changeset
   889
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
   890
  not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
42645
242bc53b98e5 do not declare TPTP built-ins, e.g. $true
blanchet
parents: 42640
diff changeset
   891
  not (String.isPrefix "$" s) andalso
42684
2123b2608b14 renamed "many_typed" to "simple" (as in simple types)
blanchet
parents: 42682
diff changeset
   892
  ((case type_sys of Simple _ => true | _ => false) orelse not pred_sym)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   893
42574
blanchet
parents: 42573
diff changeset
   894
fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
blanchet
parents: 42573
diff changeset
   895
  let
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
   896
    fun declare_sym decl decls =
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   897
      case type_sys of
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
   898
        Preds (Polymorphic, All_Types) => insert_type #3 decl decls
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   899
      | _ => insert (op =) decl decls
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
   900
    fun do_term tm =
42574
blanchet
parents: 42573
diff changeset
   901
      let val (head, args) = strip_combterm_comb tm in
blanchet
parents: 42573
diff changeset
   902
        (case head of
blanchet
parents: 42573
diff changeset
   903
           CombConst ((s, s'), T, T_args) =>
blanchet
parents: 42573
diff changeset
   904
           let val pred_sym = is_pred_sym repaired_sym_tab s in
blanchet
parents: 42573
diff changeset
   905
             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
   906
               Symtab.map_default (s, [])
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
   907
                   (declare_sym (s', T_args, T, pred_sym, length args))
42574
blanchet
parents: 42573
diff changeset
   908
             else
blanchet
parents: 42573
diff changeset
   909
               I
blanchet
parents: 42573
diff changeset
   910
           end
blanchet
parents: 42573
diff changeset
   911
         | _ => I)
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
   912
        #> fold do_term args
42574
blanchet
parents: 42573
diff changeset
   913
      end
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
   914
  in do_term end
42574
blanchet
parents: 42573
diff changeset
   915
fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   916
  fact_lift (formula_fold true
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
   917
      (K (add_combterm_syms_to_decl_table type_sys repaired_sym_tab)))
42574
blanchet
parents: 42573
diff changeset
   918
fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
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
   919
  Symtab.empty |> is_type_sys_fairly_sound type_sys
42574
blanchet
parents: 42573
diff changeset
   920
                  ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
blanchet
parents: 42573
diff changeset
   921
                         facts
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   922
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
   923
fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   924
    String.isPrefix bound_var_prefix s
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   925
  | is_var_or_bound_var (CombVar _) = true
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   926
  | is_var_or_bound_var _ = false
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   927
42685
7a5116bd63b7 documentation tuning
blanchet
parents: 42684
diff changeset
   928
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
7a5116bd63b7 documentation tuning
blanchet
parents: 42684
diff changeset
   929
   out with monotonicity" paper presented at CADE 2011. *)
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   930
fun add_combterm_nonmonotonic_types _ (SOME false) _ = I
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   931
  | add_combterm_nonmonotonic_types ctxt _
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   932
        (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   933
                  tm2)) =
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   934
    (exists is_var_or_bound_var [tm1, tm2] andalso
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   935
     not (is_type_surely_infinite ctxt T)) ? insert_type I T
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   936
  | add_combterm_nonmonotonic_types _ _ _ = I
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   937
fun add_fact_nonmonotonic_types ctxt ({kind, combformula, ...}
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   938
                                      : translated_formula) =
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   939
  formula_fold (kind <> Conjecture) (add_combterm_nonmonotonic_types ctxt)
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   940
               combformula
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   941
fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   942
  level_of_type_sys type_sys = Nonmonotonic_Types
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
   943
  ? (insert_type I @{typ bool} (* in case helper "True_or_False" is included *)
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
   944
     #> fold (add_fact_nonmonotonic_types ctxt) facts)
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
   945
42574
blanchet
parents: 42573
diff changeset
   946
fun n_ary_strip_type 0 T = ([], T)
blanchet
parents: 42573
diff changeset
   947
  | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) =
blanchet
parents: 42573
diff changeset
   948
    n_ary_strip_type (n - 1) ran_T |>> cons dom_T
blanchet
parents: 42573
diff changeset
   949
  | n_ary_strip_type _ _ = raise Fail "unexpected non-function"
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   950
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   951
fun result_type_of_decl (_, _, T, _, ary) = n_ary_strip_type ary T |> snd
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   952
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
   953
fun decl_line_for_sym s (s', _, T, pred_sym, ary) =
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   954
  let val (arg_Ts, res_T) = n_ary_strip_type ary T in
42612
bb9143d7e217 cosmetics
blanchet
parents: 42608
diff changeset
   955
    Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   956
          if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   957
  end
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   958
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
   959
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
   960
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   961
fun formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s j
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   962
                              (s', T_args, T, _, ary) =
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   963
  let
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   964
    val (arg_Ts, res_T) = n_ary_strip_type ary T
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   965
    val bound_names =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   966
      1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   967
    val bound_tms =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   968
      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
   969
    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
   970
      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
   971
                             else NONE)
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   972
  in
42612
bb9143d7e217 cosmetics
blanchet
parents: 42608
diff changeset
   973
    Formula (sym_decl_prefix ^ s ^
bb9143d7e217 cosmetics
blanchet
parents: 42608
diff changeset
   974
             (if n > 1 then "_" ^ string_of_int j else ""), Axiom,
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   975
             CombConst ((s, s'), T, T_args)
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   976
             |> fold (curry (CombApp o swap)) bound_tms
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
   977
             |> 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
   978
             |> mk_aquant AForall (bound_names ~~ bound_Ts)
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   979
             |> formula_from_combformula ctxt nonmono_Ts type_sys
42586
59e0ca92bb0b close formula universally, to make SPASS happy
blanchet
parents: 42585
diff changeset
   980
             |> close_formula_universally,
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   981
             NONE, NONE)
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   982
  end
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   983
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
   984
fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (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
   985
  case type_sys of
42684
2123b2608b14 renamed "many_typed" to "simple" (as in simple types)
blanchet
parents: 42682
diff changeset
   986
    Simple _ => map (decl_line_for_sym 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
   987
  | _ =>
42574
blanchet
parents: 42573
diff changeset
   988
    let
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   989
      val decls =
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   990
        case decls of
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   991
          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
   992
          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
   993
            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
   994
                       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
   995
              [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
   996
            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
   997
              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
   998
          end
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
   999
        | _ => decls
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1000
      val n = length decls
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1001
      val decls =
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1002
        decls |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1003
                         o result_type_of_decl)
42574
blanchet
parents: 42573
diff changeset
  1004
    in
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1005
      map2 (formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s)
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1006
           (0 upto length decls - 1) decls
42574
blanchet
parents: 42573
diff changeset
  1007
    end
42579
2552c09b1a72 implement the new ATP type system in Sledgehammer
blanchet
parents: 42577
diff changeset
  1008
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1009
fun problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys sym_decl_tab =
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1010
  Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt nonmono_Ts
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1011
                                                        type_sys)
42574
blanchet
parents: 42573
diff changeset
  1012
                  sym_decl_tab []
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1013
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1014
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
  1015
    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
  1016
  | add_tff_types_in_formula (AConn (_, phis)) =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1017
    fold add_tff_types_in_formula phis
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1018
  | add_tff_types_in_formula (AAtom _) = I
42539
f6ba908b8b27 generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents: 42538
diff changeset
  1019
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
  1020
fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
  1021
    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
  1022
  | 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
  1023
    add_tff_types_in_formula phi
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1024
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1025
fun tff_types_in_problem problem =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1026
  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
  1027
42545
a14b602fb3d5 minor cleanup
blanchet
parents: 42544
diff changeset
  1028
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
  1029
  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
  1030
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1031
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
  1032
val sym_declsN = "Symbol types"
41157
blanchet
parents: 41150
diff changeset
  1033
val factsN = "Relevant facts"
blanchet
parents: 41150
diff changeset
  1034
val class_relsN = "Class relationships"
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
  1035
val aritiesN = "Arities"
41157
blanchet
parents: 41150
diff changeset
  1036
val helpersN = "Helper facts"
blanchet
parents: 41150
diff changeset
  1037
val conjsN = "Conjectures"
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1038
val free_typesN = "Type variables"
41157
blanchet
parents: 41150
diff changeset
  1039
blanchet
parents: 41150
diff changeset
  1040
fun offset_of_heading_in_problem _ [] j = j
blanchet
parents: 41150
diff changeset
  1041
  | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
blanchet
parents: 41150
diff changeset
  1042
    if heading = needle then j
blanchet
parents: 41150
diff changeset
  1043
    else offset_of_heading_in_problem needle problem (j + length lines)
blanchet
parents: 41150
diff changeset
  1044
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
  1045
fun prepare_atp_problem ctxt type_sys explicit_apply hyp_ts concl_t facts =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1046
  let
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1047
    val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
41134
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
  1048
      translate_formulas ctxt type_sys hyp_ts concl_t facts
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
  1049
    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
  1050
    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
  1051
      [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
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
  1052
    val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab
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
  1053
    val (conjs, facts) = (conjs, facts) |> pairself (map repair)
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1054
    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
  1055
    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
  1056
      repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
42680
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1057
    val sym_decl_lines =
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: 42677
diff changeset
  1058
      conjs @ facts
b6c27cf04fe9 exploit inferred monotonicity
blanchet
parents: