src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
author blanchet
Sun, 01 May 2011 18:37:24 +0200
changeset 42544 75cb06eee990
parent 42543 f9d402d144d4
child 42545 a14b602fb3d5
permissions -rw-r--r--
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
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
40114
blanchet
parents: 40069
diff changeset
    13
  type translated_formula
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    14
41134
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
    15
  datatype type_system =
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    16
    Many_Typed |
41134
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
    17
    Tags of bool |
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    18
    Args of bool |
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    19
    Mangled of bool |
41134
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
    20
    No_Types
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
    21
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
    22
  val fact_prefix : string
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    23
  val conjecture_prefix : 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
    24
  val boolify_base : string
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
    25
  val explicit_app_base : string
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42361
diff changeset
    26
  val is_type_system_sound : type_system -> bool
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42361
diff changeset
    27
  val type_system_types_dangerous_types : 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
    28
  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
    29
  val unmangled_const : string -> string * string fo_term list
41088
54eb8e7c7f9b clarified terminology
blanchet
parents: 40204
diff changeset
    30
  val translate_atp_fact :
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
    31
    Proof.context -> bool -> (string * 'a) * thm
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
    32
    -> translated_formula option * ((string * 'a) * thm)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39975
diff changeset
    33
  val prepare_atp_problem :
42521
02df3b78a438 get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
blanchet
parents: 42520
diff changeset
    34
    Proof.context -> bool -> 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
    35
    -> (translated_formula option * ((string * 'a) * thm)) list
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
    36
    -> string problem * string Symtab.table * int * int
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
    37
       * (string * 'a) list vector
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
    38
  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
    39
end;
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    40
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
    41
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
    42
struct
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    43
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    44
open ATP_Problem
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39452
diff changeset
    45
open Metis_Translate
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    46
open Sledgehammer_Util
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    47
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    48
val type_decl_prefix = "type_"
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    49
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
    50
val fact_prefix = "fact_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    51
val conjecture_prefix = "conj_"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    52
val helper_prefix = "help_"
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    53
val class_rel_clause_prefix = "crel_";
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    54
val arity_clause_prefix = "arity_"
39975
7c50d5ca5c04 avoid generating several formulas with the same name ("tfrees")
blanchet
parents: 39954
diff changeset
    55
val tfree_prefix = "tfree_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    56
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
    57
val boolify_base = "hBOOL"
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
    58
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
    59
val type_pred_base = "is"
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
    60
val type_prefix = "ty_"
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
    61
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
    62
fun make_type ty = type_prefix ^ ascii_of ty
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
    63
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
    64
(* official TPTP TFF syntax *)
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
    65
val tff_type_of_types = "$tType"
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
    66
val tff_bool_type = "$o"
46e690db16b8 fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents: 42533
diff changeset
    67
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    68
(* Freshness almost guaranteed! *)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    69
val sledgehammer_weak_prefix = "Sledgehammer:"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    70
40114
blanchet
parents: 40069
diff changeset
    71
type translated_formula =
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38748
diff changeset
    72
  {name: string,
42525
7a506b0b644f distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree
blanchet
parents: 42524
diff changeset
    73
   kind: formula_kind,
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
    74
   combformula: (name, combtyp, combterm) formula,
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38748
diff changeset
    75
   ctypes_sorts: typ list}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    76
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
    77
fun map_combformula f
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
    78
        ({name, kind, combformula, ctypes_sorts} : translated_formula) =
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
    79
  {name = name, kind = kind, combformula = f combformula,
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
   ctypes_sorts = ctypes_sorts} : translated_formula
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
    81
41134
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
    82
datatype type_system =
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    83
  Many_Typed |
41134
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
    84
  Tags of bool |
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    85
  Args of bool |
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    86
  Mangled of bool |
41134
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
    87
  No_Types
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
    88
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    89
fun is_type_system_sound Many_Typed = true
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    90
  | is_type_system_sound (Tags full_types) = full_types
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    91
  | is_type_system_sound (Args full_types) = full_types
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    92
  | is_type_system_sound (Mangled full_types) = full_types
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    93
  | is_type_system_sound No_Types = false
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42361
diff changeset
    94
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42361
diff changeset
    95
fun type_system_types_dangerous_types (Tags _) = true
42523
08346ea46a59 added (without implementation yet) new type encodings for Sledgehammer/ATP
blanchet
parents: 42522
diff changeset
    96
  | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
    97
42524
3df98f0de5a0 remove experimental feature ("risky overload")
blanchet
parents: 42523
diff changeset
    98
fun dont_need_type_args type_sys 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
    99
  s <> type_pred_base andalso
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
   100
  (member (op =) [@{const_name HOL.eq}] s orelse
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   101
   case type_sys of
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   102
     Many_Typed => false
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   103
   | Tags full_types => full_types orelse s = explicit_app_base
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   104
   | Args _ => s = explicit_app_base
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   105
   | Mangled _ => s = explicit_app_base
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   106
   | No_Types => true)
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
   107
42227
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 42180
diff changeset
   108
datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 42180
diff changeset
   109
42524
3df98f0de5a0 remove experimental feature ("risky overload")
blanchet
parents: 42523
diff changeset
   110
fun type_arg_policy type_sys s =
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   111
  if dont_need_type_args type_sys s then
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   112
    No_Type_Args
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   113
  else
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   114
    case type_sys of
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   115
      Many_Typed => Mangled_Types
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   116
    | Mangled _ => Mangled_Types
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   117
    | _ => Explicit_Type_Args
42227
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 42180
diff changeset
   118
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
   119
fun num_atp_type_args thy type_sys s =
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   120
  if type_arg_policy type_sys s = Explicit_Type_Args then
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
   121
    if s = type_pred_base then 1 else num_type_args thy s
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   122
  else
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   123
    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
   124
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
   125
fun atp_type_literals_for_types type_sys kind Ts =
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
   126
  if type_sys = No_Types then
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
   127
    []
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
   128
  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
   129
    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
   130
       |> 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
   131
                   | 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
   132
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   133
fun mk_anot phi = AConn (ANot, [phi])
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   134
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
   135
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
   136
  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
   137
    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
   138
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   139
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
   140
  | 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
   141
fun mk_aquant _ [] phi = phi
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   142
  | 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
   143
    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
   144
  | 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
   145
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   146
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
   147
  let
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   148
    fun formula_vars bounds (AQuant (_, xs, phi)) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   149
        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
   150
      | 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
   151
      | formula_vars bounds (AAtom tm) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   152
        union (op =) (atom_vars tm []
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   153
                      |> 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
   154
  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
   155
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   156
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
   157
  | combterm_vars (CombConst _) = I
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   158
  | combterm_vars (CombVar (name, ty)) = insert (op =) (name, SOME ty)
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   159
val close_combformula_universally = close_universally combterm_vars
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   160
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   161
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
   162
  is_atp_variable s ? insert (op =) (name, NONE)
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   163
  #> fold term_vars tms
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   164
val close_formula_universally = close_universally term_vars
41145
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   165
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
   166
(* We are crossing our fingers that it doesn't clash with anything else. *)
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
   167
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
   168
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
   169
fun mangled_combtyp_component f (CombTFree name) = f name
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
   170
  | mangled_combtyp_component f (CombTVar name) =
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
   171
    f name (* FIXME: shouldn't happen *)
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
   172
    (* raise Fail "impossible schematic type variable" *)
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
   173
  | mangled_combtyp_component f (CombType (name, tys)) =
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
   174
    f name ^ "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")"
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
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
   176
fun mangled_combtyp ty =
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
   177
  (make_type (mangled_combtyp_component fst ty),
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
   178
   mangled_combtyp_component snd ty)
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
   179
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
   180
fun mangled_type_suffix f g tys =
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
   181
  fold_rev (curry (op ^) o g o prefix mangled_type_sep
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
   182
            o mangled_combtyp_component f) tys ""
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
   183
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
   184
fun mangled_const_name_fst ty_args 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
   185
  s ^ mangled_type_suffix fst ascii_of ty_args
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
   186
fun mangled_const_name_snd ty_args s' = s' ^ mangled_type_suffix snd I ty_args
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
   187
fun mangled_const_name ty_args (s, 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
   188
  (mangled_const_name_fst ty_args s, mangled_const_name_snd ty_args 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
   189
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
   190
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
   191
  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
   192
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
   193
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
   194
  (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
   195
   -- 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
   196
                    [] >> 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
   197
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
   198
  (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
   199
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
   200
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
   201
  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
   202
    |> 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
   203
           (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
   204
                                                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
   205
    |> 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
   206
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
   207
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
   208
  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
   209
    (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
   210
  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
   211
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   212
fun combformula_for_prop thy eq_as_iff =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   213
  let
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   214
    fun do_term bs t ts =
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   215
      combterm_from_term thy bs (Envir.eta_contract t)
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   216
      |>> AAtom ||> union (op =) ts
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   217
    fun do_quant bs q s T t' =
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   218
      let val s = Name.variant (map fst bs) s in
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   219
        do_formula ((s, T) :: bs) t'
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   220
        #>> mk_aquant q [(`make_bound_var s, SOME (combtyp_from_typ T))]
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   221
      end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   222
    and do_conn bs c t1 t2 =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   223
      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
   224
      #>> uncurry (mk_aconn c)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   225
    and do_formula bs t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   226
      case t of
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   227
        @{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
   228
      | 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
   229
        do_quant bs AForall s T t'
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   230
      | 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
   231
        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
   232
      | @{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
   233
      | @{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
   234
      | @{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
   235
      | 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
   236
        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
   237
      | _ => do_term bs t
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   238
  in do_formula [] end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   239
38618
5536897d04c2 remove trivial facts
blanchet
parents: 38613
diff changeset
   240
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
   241
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41406
diff changeset
   242
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
   243
fun conceal_bounds Ts t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   244
  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
   245
                    (0 upto length Ts - 1 ~~ Ts), t)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   246
fun reveal_bounds Ts =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   247
  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
   248
                    (0 upto length Ts - 1 ~~ Ts))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   249
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
   250
(* Removes the lambdas from an equation of the form "t = (%x. u)".
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39886
diff changeset
   251
   (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
   252
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
   253
  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
   254
    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
   255
      | 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
   256
                                        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
   257
                    $ t2 $ Abs (var_s, var_T, t')) =
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   258
        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
   259
          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
   260
            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
   261
              $ 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
   262
            |> 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
   263
          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
   264
        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
   265
          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
   266
      | 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
   267
  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
   268
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   269
fun introduce_combinators_in_term ctxt kind t =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   270
  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
   271
    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
   272
      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
   273
    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
   274
      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
   275
        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
   276
          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
   277
            @{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
   278
          | (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
   279
            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
   280
          | (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
   281
            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
   282
          | (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
   283
            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
   284
          | (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
   285
            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
   286
          | (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
   287
          | (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
   288
          | (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
   289
          | (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
   290
              $ 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
   291
            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
   292
          | _ => 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
   293
                   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
   294
                 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
   295
                   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
   296
                     |> 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
   297
                     |> cterm_of thy
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39886
diff changeset
   298
                     |> 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
   299
                     |> 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
   300
                     |> reveal_bounds Ts
39370
f8292d3020db use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents: 39005
diff changeset
   301
        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
   302
      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
   303
      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
   304
             (* 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
   305
             if kind = Conjecture then HOLogic.false_const
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   306
             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
   307
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   308
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   309
(* 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
   310
   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
   311
fun freeze_term t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   312
  let
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   313
    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
   314
      | 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
   315
      | aux (Var ((s, i), T)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   316
        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
   317
      | aux t = t
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   318
  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
   319
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
   320
(* making fact and conjecture formulas *)
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   321
fun make_formula ctxt eq_as_iff presimp name kind t =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   322
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   323
    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
   324
    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
   325
              |> transform_elim_term
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41199
diff changeset
   326
              |> Object_Logic.atomize_term thy
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38618
diff changeset
   327
    val need_trueprop = (fastype_of t = HOLogic.boolT)
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38618
diff changeset
   328
    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
   329
              |> extensionalize_term
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   330
              |> presimp ? presimplify_term thy
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   331
              |> perhaps (try (HOLogic.dest_Trueprop))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   332
              |> introduce_combinators_in_term ctxt kind
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   333
              |> kind <> Axiom ? freeze_term
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
   334
    val (combformula, ctypes_sorts) =
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   335
      combformula_for_prop thy eq_as_iff t []
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   336
  in
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38748
diff changeset
   337
    {name = name, combformula = combformula, kind = kind,
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38748
diff changeset
   338
     ctypes_sorts = ctypes_sorts}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   339
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   340
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   341
fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), th) =
41990
7f2793d51efc add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents: 41770
diff changeset
   342
  case (keep_trivial,
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   343
        make_formula ctxt eq_as_iff presimp name Axiom (prop_of th)) of
41990
7f2793d51efc add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents: 41770
diff changeset
   344
    (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
   345
    NONE
7f2793d51efc add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents: 41770
diff changeset
   346
  | (_, formula) => SOME formula
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   347
fun make_conjecture ctxt ts =
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   348
  let val last = length ts - 1 in
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   349
    map2 (fn j => make_formula ctxt true true (string_of_int j)
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   350
                               (if j = last then Conjecture else Hypothesis))
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   351
         (0 upto last) ts
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   352
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   353
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   354
(** Helper facts **)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   355
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
   356
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
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
   357
  | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
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
   358
  | formula_map f (AAtom tm) = AAtom (f tm)
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
   359
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
   360
fun formula_fold f (AQuant (_, _, phi)) = formula_fold f phi
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
   361
  | formula_fold f (AConn (_, phis)) = fold (formula_fold f) phis
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
   362
  | formula_fold f (AAtom tm) = f tm
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   363
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   364
fun count_term (ATerm ((s, _), tms)) =
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
   365
  (if is_atp_variable s then I else Symtab.map_entry s (Integer.add 1))
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   366
  #> fold count_term tms
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
   367
fun count_formula x = formula_fold count_term x
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   368
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   369
val init_counters =
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   370
  metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0)
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   371
  |> Symtab.make
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   372
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
   373
(* ### FIXME: do this on repaired combterms *)
42521
02df3b78a438 get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
blanchet
parents: 42520
diff changeset
   374
fun get_helper_facts ctxt type_sys formulas =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   375
  let
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42361
diff changeset
   376
    val no_dangerous_types = type_system_types_dangerous_types type_sys
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   377
    val ct = init_counters |> fold count_formula formulas
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   378
    fun is_used s = the (Symtab.lookup ct s) > 0
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   379
    fun dub c needs_full_types (th, j) =
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   380
      ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   381
        false), th)
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   382
    fun make_facts eq_as_iff = map_filter (make_fact ctxt false eq_as_iff false)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   383
  in
41145
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   384
    (metis_helpers
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   385
     |> filter (is_used o fst)
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   386
     |> maps (fn (c, (needs_full_types, ths)) =>
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   387
                 if needs_full_types andalso not no_dangerous_types then
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   388
                   []
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   389
                 else
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   390
                   ths ~~ (1 upto length ths)
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   391
                   |> map (dub c needs_full_types)
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   392
                   |> make_facts (not needs_full_types)),
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   393
     if type_sys = Tags false then
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   394
       let
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   395
         fun var s = ATerm (`I s, [])
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   396
         fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   397
       in
42538
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   398
         [Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom,
42527
6a9458524f01 reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents: 42526
diff changeset
   399
                   AAtom (ATerm (`I "equal",
6a9458524f01 reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents: 42526
diff changeset
   400
                                 [tag (tag (var "Y")), tag (var "Y")]))
42529
747736d8b47e added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS
blanchet
parents: 42528
diff changeset
   401
                   |> close_formula_universally, NONE, NONE)]
41145
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   402
       end
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   403
     else
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   404
       [])
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   405
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   406
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   407
fun translate_atp_fact ctxt keep_trivial =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   408
  `(make_fact ctxt keep_trivial true true)
39004
f1b465f889b5 translate the axioms to FOF once and for all ATPs
blanchet
parents: 39003
diff changeset
   409
41134
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
   410
fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   411
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   412
    val thy = Proof_Context.theory_of ctxt
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
   413
    val fact_ts = map (prop_of o snd o snd) rich_facts
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
   414
    val (facts, fact_names) =
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
   415
      rich_facts
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
   416
      |> map_filter (fn (NONE, _) => NONE
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
   417
                      | (SOME fact, (name, _)) => SOME (fact, name))
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41088
diff changeset
   418
      |> ListPair.unzip
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
   419
    (* Remove existing facts from the conjecture, as this can dramatically
39005
42fcb25de082 minor refactoring
blanchet
parents: 39004
diff changeset
   420
       boost an ATP's performance (for some reason). *)
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
   421
    val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   422
    val goal_t = Logic.list_implies (hyp_ts, concl_t)
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
   423
    val all_ts = goal_t :: fact_ts
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
   424
    val subs = tfree_classes_of_terms all_ts
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
   425
    val supers = tvar_classes_of_terms all_ts
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
   426
    val tycons = type_consts_of_terms thy all_ts
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   427
    val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
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
   428
    val (supers', arity_clauses) =
8b634031b2a5 implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents: 41136
diff changeset
   429
      if type_sys = No_Types then ([], [])
8b634031b2a5 implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents: 41136
diff changeset
   430
      else make_arity_clauses thy tycons supers
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   431
    val class_rel_clauses = make_class_rel_clauses thy subs supers'
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   432
  in
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   433
    (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   434
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   435
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   436
fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t])
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   437
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   438
fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   439
  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   440
  | fo_term_for_combtyp (CombType (name, tys)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   441
    ATerm (name, map fo_term_for_combtyp tys)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   442
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   443
fun fo_literal_for_type_literal (TyLitVar (class, name)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   444
    (true, ATerm (class, [ATerm (name, [])]))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   445
  | fo_literal_for_type_literal (TyLitFree (class, name)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   446
    (true, ATerm (class, [ATerm (name, [])]))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   447
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   448
fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   449
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   450
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   451
   considered dangerous because their "exhaust" properties can easily lead to
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   452
   unsound ATP proofs. The checks below are an (unsound) approximation of
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   453
   finiteness. *)
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   454
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   455
fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   456
  | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) =
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   457
    is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   458
  | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   459
and is_type_dangerous ctxt (Type (s, Ts)) =
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   460
    is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   461
  | is_type_dangerous _ _ = false
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   462
and is_type_constr_dangerous ctxt s =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   463
  let val thy = Proof_Context.theory_of ctxt in
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   464
    case Datatype_Data.get_info thy s of
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   465
      SOME {descr, ...} =>
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   466
      forall (fn (_, (_, _, constrs)) =>
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   467
                 forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   468
    | NONE =>
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   469
      case Typedef.get_info ctxt s of
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   470
        ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   471
      | [] => true
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   472
  end
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   473
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   474
fun is_combtyp_dangerous ctxt (CombType ((s, _), tys)) =
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   475
    (case strip_prefix_and_unascii type_const_prefix s of
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   476
       SOME s' => forall (is_combtyp_dangerous ctxt) tys andalso
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   477
                  is_type_constr_dangerous ctxt (invert_const s')
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   478
     | NONE => false)
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   479
  | is_combtyp_dangerous _ _ = false
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   480
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   481
fun should_tag_with_type ctxt (Tags full_types) ty =
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   482
    full_types orelse is_combtyp_dangerous ctxt ty
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   483
  | should_tag_with_type _ _ _ = false
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   484
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   485
val fname_table =
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   486
  [("c_False", (0, ("c_fFalse", @{const_name Metis.fFalse}))),
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   487
   ("c_True", (0, ("c_fTrue", @{const_name Metis.fTrue}))),
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   488
   ("c_Not", (1, ("c_fNot", @{const_name Metis.fNot}))),
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   489
   ("c_conj", (2, ("c_fconj", @{const_name Metis.fconj}))),
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   490
   ("c_disj", (2, ("c_fdisj", @{const_name Metis.fdisj}))),
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   491
   ("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))),
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   492
   ("equal", (2, ("c_fequal", @{const_name Metis.fequal})))]
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   493
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   494
fun repair_combterm_consts type_sys =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   495
  let
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   496
    fun aux (CombApp tmp) = CombApp (pairself aux tmp)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   497
      | aux (CombConst (name as (s, _), ty, ty_args)) =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   498
        (case strip_prefix_and_unascii const_prefix s of
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   499
           NONE => (name, ty_args)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   500
         | SOME s'' =>
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   501
           let val s'' = invert_const s'' in
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   502
             case type_arg_policy type_sys s'' of
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   503
               No_Type_Args => (name, [])
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   504
             | Explicit_Type_Args => (name, ty_args)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   505
             | Mangled_Types => (mangled_const_name ty_args name, [])
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   506
           end)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   507
        |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   508
      | aux tm = tm
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   509
  in aux end
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   510
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   511
fun pred_combtyp ty =
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   512
  case combtyp_from_typ @{typ "unit => bool"} of
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   513
    CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty])
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   514
  | _ => raise Fail "expected two-argument type constructor"
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   515
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
   516
fun type_pred_combatom type_sys ty tm =
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
   517
  CombApp (CombConst ((const_prefix ^ type_pred_base, type_pred_base),
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
   518
                      pred_combtyp ty, [ty]), tm)
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
   519
  |> repair_combterm_consts type_sys
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
   520
  |> AAtom
46e690db16b8 fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents: 42533
diff changeset
   521
42530
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   522
fun formula_for_combformula ctxt type_sys =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   523
  let
42530
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   524
    fun do_term top_level u =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   525
      let
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   526
        val (head, args) = strip_combterm_comb u
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   527
        val (x, ty_args) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   528
          case head of
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   529
            CombConst (name as (s, s'), _, ty_args) =>
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   530
            (case AList.lookup (op =) fname_table s of
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   531
               SOME (n, fname) =>
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
   532
(*### FIXME: do earlier? *)
41150
54b3c9c05664 make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
blanchet
parents: 41149
diff changeset
   533
               (if top_level andalso length args = n then
54b3c9c05664 make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
blanchet
parents: 41149
diff changeset
   534
                  case s of
54b3c9c05664 make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
blanchet
parents: 41149
diff changeset
   535
                    "c_False" => ("$false", s')
54b3c9c05664 make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
blanchet
parents: 41149
diff changeset
   536
                  | "c_True" => ("$true", s')
54b3c9c05664 make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
blanchet
parents: 41149
diff changeset
   537
                  | _ => name
54b3c9c05664 make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
blanchet
parents: 41149
diff changeset
   538
                else
54b3c9c05664 make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
blanchet
parents: 41149
diff changeset
   539
                  fname, [])
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
   540
             | NONE => (name, ty_args))
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   541
          | CombVar (name, _) => (name, [])
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   542
          | CombApp _ => raise Fail "impossible \"CombApp\""
42530
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   543
        val t = ATerm (x, map fo_term_for_combtyp ty_args @
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   544
                          map (do_term false) args)
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   545
        val ty = combtyp_of u
42530
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   546
      in
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   547
        t |> (if should_tag_with_type ctxt type_sys ty then
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   548
                tag_with_type (fo_term_for_combtyp ty)
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   549
              else
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   550
                I)
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   551
      end
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   552
    val do_bound_type =
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   553
      if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   554
    val do_out_of_bound_type =
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   555
      if member (op =) [Args true, Mangled true] type_sys then
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   556
        (fn (s, 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
   557
            type_pred_combatom type_sys ty (CombVar (s, ty))
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
   558
            |> formula_for_combformula ctxt type_sys |> SOME)
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   559
      else
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   560
        K NONE
42530
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   561
    fun do_formula (AQuant (q, xs, phi)) =
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   562
        AQuant (q, xs |> map (apsnd (fn NONE => NONE
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   563
                                      | SOME ty => do_bound_type ty)),
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
   564
                (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   565
                    (map_filter
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   566
                         (fn (_, NONE) => NONE
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   567
                           | (s, SOME ty) => do_out_of_bound_type (s, ty)) xs)
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   568
                    (do_formula phi))
42530
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   569
      | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   570
      | do_formula (AAtom tm) = AAtom (do_term true tm)
f64c546efe8c fixed type of ATP quantifier types (sic)
blanchet
parents: 42529
diff changeset
   571
  in do_formula end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   572
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   573
fun formula_for_fact ctxt type_sys
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
   574
                     ({combformula, ctypes_sorts, ...} : translated_formula) =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   575
  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
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
   576
                (atp_type_literals_for_types type_sys Axiom ctypes_sorts))
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   577
           (formula_for_combformula ctxt type_sys
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   578
                                    (close_combformula_universally combformula))
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
   579
  |> close_formula_universally
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   580
42538
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   581
fun logic_for_type_sys Many_Typed = Tff
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   582
  | logic_for_type_sys _ = Fof
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   583
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41990
diff changeset
   584
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41990
diff changeset
   585
   of monomorphization). The TPTP explicitly forbids name clashes, and some of
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41990
diff changeset
   586
   the remote provers might care. *)
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41990
diff changeset
   587
fun problem_line_for_fact ctxt prefix type_sys
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41990
diff changeset
   588
                          (j, formula as {name, kind, ...}) =
42538
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   589
  Formula (logic_for_type_sys type_sys,
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   590
           prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   591
           formula_for_fact ctxt type_sys formula, NONE, NONE)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   592
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   593
fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   594
                                                       superclass, ...}) =
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
   595
  let val ty_arg = ATerm (`I "T", []) in
42538
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   596
    Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
42527
6a9458524f01 reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents: 42526
diff changeset
   597
             AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
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
   598
                               AAtom (ATerm (superclass, [ty_arg]))])
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
   599
             |> close_formula_universally, NONE, NONE)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   600
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   601
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   602
fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   603
    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   604
  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   605
    (false, ATerm (c, [ATerm (sort, [])]))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   606
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   607
fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   608
                                                ...}) =
42538
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   609
  Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
42527
6a9458524f01 reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents: 42526
diff changeset
   610
           mk_ahorn (map (formula_for_fo_literal o apfst not
6a9458524f01 reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents: 42526
diff changeset
   611
                          o fo_literal_for_arity_literal) premLits)
6a9458524f01 reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents: 42526
diff changeset
   612
                    (formula_for_fo_literal
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
   613
                         (fo_literal_for_arity_literal conclLit))
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
   614
           |> close_formula_universally, NONE, NONE)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   615
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41137
diff changeset
   616
fun problem_line_for_conjecture ctxt type_sys
40114
blanchet
parents: 40069
diff changeset
   617
        ({name, kind, combformula, ...} : translated_formula) =
42538
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   618
  Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
42527
6a9458524f01 reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents: 42526
diff changeset
   619
           formula_for_combformula ctxt type_sys
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
   620
                                   (close_combformula_universally combformula)
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
   621
           |> close_formula_universally, NONE, NONE)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   622
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
   623
fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) =
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
   624
  ctypes_sorts |> atp_type_literals_for_types type_sys 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
   625
               |> map fo_literal_for_type_literal
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   626
39975
7c50d5ca5c04 avoid generating several formulas with the same name ("tfrees")
blanchet
parents: 39954
diff changeset
   627
fun problem_line_for_free_type j lit =
42538
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   628
  Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis,
42529
747736d8b47e added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS
blanchet
parents: 42528
diff changeset
   629
           formula_for_fo_literal lit, NONE, NONE)
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
   630
fun problem_lines_for_free_types type_sys facts =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   631
  let
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
   632
    val litss = map (free_type_literals type_sys) facts
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   633
    val lits = fold (union (op =)) litss []
39975
7c50d5ca5c04 avoid generating several formulas with the same name ("tfrees")
blanchet
parents: 39954
diff changeset
   634
  in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   635
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   636
(** "hBOOL" and "hAPP" **)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   637
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   638
type repair_info = {pred_sym: bool, min_arity: int, max_arity: int}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   639
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   640
fun consider_combterm_for_repair top_level 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
   641
  let val (head, args) = strip_combterm_comb tm 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
   642
    (case head 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
   643
       CombConst ((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
   644
       if String.isPrefix bound_var_prefix s then
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
   645
         I
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
   646
       else
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
   647
         let val n = length args 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
   648
           Symtab.map_default
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   649
               (s, {pred_sym = true, min_arity = n, max_arity = 0})
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   650
               (fn {pred_sym, min_arity, max_arity} =>
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   651
                   {pred_sym = pred_sym andalso top_level,
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   652
                    min_arity = Int.min (n, min_arity),
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   653
                    max_arity = Int.max (n, max_arity)})
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
   654
        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
   655
     | _ => I)
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   656
    #> fold (consider_combterm_for_repair false) args
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
   657
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   658
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   659
fun consider_fact_for_repair ({combformula, ...} : translated_formula) =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   660
  formula_fold (consider_combterm_for_repair true) combformula
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   661
42539
f6ba908b8b27 generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents: 42538
diff changeset
   662
(* The "equal" entry is needed for helper facts if the problem otherwise does
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   663
   not involve equality. The "hBOOL" and "hAPP" entries are needed for symbol
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   664
   declarations. *)
42539
f6ba908b8b27 generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents: 42538
diff changeset
   665
val default_entries =
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   666
  [("equal", {pred_sym = true, min_arity = 2, max_arity = 2}),
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   667
   (make_fixed_const boolify_base,
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   668
    {pred_sym = true, min_arity = 1, max_arity = 1}),
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   669
   (make_fixed_const explicit_app_base,
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   670
    {pred_sym = false, min_arity = 2, max_arity = 2})]
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   671
(* FIXME: last two entries needed? ### *)
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   672
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   673
fun sym_table_for_facts explicit_apply facts =
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   674
  if explicit_apply then
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   675
    NONE
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   676
  else
42539
f6ba908b8b27 generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents: 42538
diff changeset
   677
    SOME (Symtab.empty |> fold Symtab.default default_entries
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   678
                       |> fold consider_fact_for_repair facts)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   679
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   680
fun min_arity_of _ _ (SOME sym_tab) s =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   681
    (case Symtab.lookup sym_tab s of
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   682
       SOME ({min_arity, ...} : repair_info) => min_arity
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   683
     | NONE => 0)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   684
  | min_arity_of thy type_sys NONE s =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   685
    if s = "equal" orelse s = type_tag_name orelse
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   686
       String.isPrefix type_const_prefix s orelse
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   687
       String.isPrefix class_prefix s then
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   688
      16383 (* large number *)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   689
    else case strip_prefix_and_unascii const_prefix s of
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   690
      SOME s' => s' |> unmangled_const |> fst |> invert_const
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   691
                    |> num_atp_type_args thy type_sys
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   692
    | NONE => 0
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   693
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   694
(* 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
   695
   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
   696
   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
   697
   arguments and is used as a predicate. *)
42520
d1f7c4a01dbe renamings
blanchet
parents: 42449
diff changeset
   698
fun is_pred_sym NONE s =
38589
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38518
diff changeset
   699
    s = "equal" orelse s = "$false" orelse s = "$true" orelse
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38518
diff changeset
   700
    String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix 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
   701
  | is_pred_sym (SOME sym_tab) s =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   702
    case Symtab.lookup sym_tab s of
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   703
      SOME {pred_sym, min_arity, max_arity} =>
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
   704
      pred_sym andalso min_arity = max_arity
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   705
    | NONE => false
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   706
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
   707
val boolify_combconst =
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   708
  CombConst (`make_fixed_const boolify_base,
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   709
             combtyp_from_typ @{typ "bool => bool"}, [])
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   710
fun boolify tm = CombApp (boolify_combconst, tm)
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
   711
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   712
fun repair_pred_syms_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
   713
  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
   714
    (CombConst ((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
   715
    if is_pred_sym sym_tab s then tm else boolify 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
   716
  | _ => boolify tm
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
   717
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   718
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
   719
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   720
val fun_name = `make_fixed_type_const @{type_name fun}
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   721
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   722
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
   723
  let
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   724
    val head_ty = combtyp_of head
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   725
    val (arg_ty, res_ty) = dest_combfun head_ty
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   726
    val 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
   727
      CombConst (`make_fixed_const explicit_app_base,
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   728
                 CombType (fun_name, [head_ty, head_ty]), [arg_ty, res_ty])
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   729
  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
   730
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
   731
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   732
fun repair_apps_in_combterm thy type_sys sym_tab =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   733
  let
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   734
    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
   735
      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
   736
        (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
   737
        args |> map aux
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   738
             |> chop (min_arity_of thy type_sys sym_tab s)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   739
             |>> 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
   740
             |-> 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
   741
      | (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
   742
  in aux end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   743
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   744
fun repair_combterm thy type_sys sym_tab =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   745
  (case type_sys of Tags _ => I | _ => repair_pred_syms_in_combterm sym_tab)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   746
  #> repair_apps_in_combterm thy type_sys sym_tab
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   747
  #> repair_combterm_consts type_sys
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   748
val repair_combformula = formula_map ooo repair_combterm
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   749
val repair_fact = map_combformula ooo repair_combformula
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   750
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   751
fun is_const_relevant type_sys sym_tab 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
   752
  not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   753
  (type_sys = Many_Typed orelse not (is_pred_sym sym_tab s))
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   754
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   755
fun consider_combterm_consts type_sys sym_tab tm =
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   756
  let val (head, args) = strip_combterm_comb tm in
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   757
    (case head of
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   758
       CombConst ((s, s'), ty, ty_args) =>
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   759
       (* FIXME: exploit type subsumption *)
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   760
       is_const_relevant type_sys sym_tab s
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
   761
       ? Symtab.insert_list (op =) (s, (s', ty_args, ty))
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   762
     | _ => I)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   763
    #> fold (consider_combterm_consts type_sys sym_tab) args
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   764
  end
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   765
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   766
fun consider_fact_consts type_sys sym_tab
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
   767
                         ({combformula, ...} : translated_formula) =
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   768
  formula_fold (consider_combterm_consts type_sys sym_tab) combformula
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   769
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   770
fun const_table_for_facts type_sys sym_tab facts =
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   771
  Symtab.empty |> member (op =) [Many_Typed, Args true, Mangled true] type_sys
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   772
                  ? fold (consider_fact_consts type_sys sym_tab) facts
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   773
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   774
fun strip_and_map_combtyp 0 f ty = ([], f ty)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   775
  | strip_and_map_combtyp n f (ty as CombType ((s, _), tys)) =
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   776
    (case (strip_prefix_and_unascii type_const_prefix s, tys) of
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   777
       (SOME @{type_name fun}, [dom_ty, ran_ty]) =>
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   778
       strip_and_map_combtyp (n - 1) f ran_ty |>> cons (f dom_ty)
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
   779
     | _ => ([], f ty))
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   780
  | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function"
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   781
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   782
fun sym_decl_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   783
  let
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   784
    val thy = Proof_Context.theory_of ctxt
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   785
    val arity = min_arity_of thy type_sys sym_tab s
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   786
  in
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   787
    if type_sys = Many_Typed then
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   788
      let
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   789
        val (arg_tys, res_ty) = strip_and_map_combtyp arity mangled_combtyp ty
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   790
        val (s, s') = (s, s') |> mangled_const_name ty_args
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   791
      in
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   792
        Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   793
              if is_pred_sym sym_tab s then `I tff_bool_type else res_ty)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   794
      end
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   795
    else
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   796
      let
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   797
        val (arg_tys, res_ty) = strip_and_map_combtyp arity I ty
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   798
        val bounds =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   799
          map (`I o make_bound_var o string_of_int) (1 upto length arg_tys)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   800
          ~~ map SOME arg_tys
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   801
        val bound_tms =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   802
          map (fn (name, ty) => CombConst (name, the ty, [])) bounds
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   803
      in
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   804
        Formula (Fof, sym_decl_prefix ^ ascii_of s, Axiom,
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   805
                 CombConst ((s, s'), ty, ty_args)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   806
                 |> fold (curry (CombApp o swap)) bound_tms
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   807
                 |> type_pred_combatom type_sys res_ty
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   808
                 |> mk_aquant AForall bounds
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   809
                 |> formula_for_combformula ctxt type_sys,
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   810
                 NONE, NONE)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   811
      end
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   812
  end
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   813
fun sym_decl_lines_for_const ctxt type_sys sym_tab (s, xs) =
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   814
  map (sym_decl_line_for_const_entry ctxt type_sys sym_tab s) xs
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   815
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   816
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
   817
    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
   818
  | add_tff_types_in_formula (AConn (_, phis)) =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   819
    fold add_tff_types_in_formula phis
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   820
  | add_tff_types_in_formula (AAtom _) = I
42539
f6ba908b8b27 generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents: 42538
diff changeset
   821
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   822
fun add_tff_types_in_problem_line (Decl (_, _, arg_tys, res_ty)) =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   823
    union (op =) (res_ty :: arg_tys)
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   824
  | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   825
    add_tff_types_in_formula phi
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   826
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   827
fun tff_types_in_problem problem =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   828
  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
   829
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   830
fun problem_line_for_tff_type (s, s') =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   831
  Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tff_type_of_types)
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   832
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   833
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
   834
val sym_declsN = "Symbol types"
41157
blanchet
parents: 41150
diff changeset
   835
val factsN = "Relevant facts"
blanchet
parents: 41150
diff changeset
   836
val class_relsN = "Class relationships"
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   837
val aritiesN = "Arities"
41157
blanchet
parents: 41150
diff changeset
   838
val helpersN = "Helper facts"
blanchet
parents: 41150
diff changeset
   839
val conjsN = "Conjectures"
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   840
val free_typesN = "Type variables"
41157
blanchet
parents: 41150
diff changeset
   841
blanchet
parents: 41150
diff changeset
   842
fun offset_of_heading_in_problem _ [] j = j
blanchet
parents: 41150
diff changeset
   843
  | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
blanchet
parents: 41150
diff changeset
   844
    if heading = needle then j
blanchet
parents: 41150
diff changeset
   845
    else offset_of_heading_in_problem needle problem (j + length lines)
blanchet
parents: 41150
diff changeset
   846
42521
02df3b78a438 get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
blanchet
parents: 42520
diff changeset
   847
fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts
02df3b78a438 get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
blanchet
parents: 42520
diff changeset
   848
                        concl_t facts =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   849
  let
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   850
    val thy = Proof_Context.theory_of ctxt
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   851
    val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
41134
de9e0adc21da added "type_sys" option to Sledgehammer
blanchet
parents: 41091
diff changeset
   852
      translate_formulas ctxt type_sys hyp_ts concl_t facts
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   853
    val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   854
    val conjs = map (repair_fact thy type_sys sym_tab) conjs
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   855
    val facts = map (repair_fact thy type_sys sym_tab) facts
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   856
    val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   857
    (* Reordering these might confuse the proof reconstruction code or the SPASS
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   858
       Flotter hack. *)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   859
    val problem =
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
   860
      [(type_declsN, []),
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   861
       (sym_declsN, []),
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
   862
       (factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
42180
a6c141925a8a added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
blanchet
parents: 41990
diff changeset
   863
                    (0 upto length facts - 1 ~~ facts)),
41157
blanchet
parents: 41150
diff changeset
   864
       (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
blanchet
parents: 41150
diff changeset
   865
       (aritiesN, map problem_line_for_arity_clause arity_clauses),
blanchet
parents: 41150
diff changeset
   866
       (helpersN, []),
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   867
       (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
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
   868
       (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
42521
02df3b78a438 get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
blanchet
parents: 42520
diff changeset
   869
    val helper_facts =
42538
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   870
      problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi
42528
a15f0db2bcaf added support for TFF type declarations
blanchet
parents: 42527
diff changeset
   871
                                    | _ => NONE) o snd)
42527
6a9458524f01 reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
blanchet
parents: 42526
diff changeset
   872
              |> get_helper_facts ctxt type_sys
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   873
              |>> map (repair_fact thy type_sys sym_tab)
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   874
    val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   875
    val sym_decl_lines =
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
   876
      Symtab.fold_rev (append o sym_decl_lines_for_const ctxt type_sys sym_tab)
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
   877
                      const_tab []
41157
blanchet
parents: 41150
diff changeset
   878
    val helper_lines =
42521
02df3b78a438 get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
blanchet
parents: 42520
diff changeset
   879
      helper_facts
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
   880
      |>> map (pair 0 #> problem_line_for_fact ctxt helper_prefix type_sys)
41157
blanchet
parents: 41150
diff changeset
   881
      |> op @
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   882
    val problem =
42533
dc81fe6b7a87 generate TFF type declarations in typed mode
blanchet
parents: 42531
diff changeset
   883
      problem |> fold (AList.update (op =))
42543
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   884
                      [(sym_declsN, sym_decl_lines),
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   885
                       (helpersN, helper_lines)]
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   886
    val type_decl_lines =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   887
      if type_sys = Many_Typed then
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   888
        problem |> tff_types_in_problem |> map problem_line_for_tff_type
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   889
      else
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   890
        []
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   891
    val (problem, pool) =
f9d402d144d4 declare TFF types so that SNARK can be used with types
blanchet
parents: 42542
diff changeset
   892
      problem |> AList.update (op =) (type_declsN, type_decl_lines)
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   893
              |> nice_atp_problem readable_names
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   894
  in
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   895
    (problem,
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   896
     case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
   897
     offset_of_heading_in_problem factsN problem 0,
41157
blanchet
parents: 41150
diff changeset
   898
     offset_of_heading_in_problem conjsN problem 0,
blanchet
parents: 41150
diff changeset
   899
     fact_names |> Vector.fromList)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   900
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   901
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   902
(* FUDGE *)
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   903
val conj_weight = 0.0
41770
a710e96583d5 adjust fudge factors
blanchet
parents: 41769
diff changeset
   904
val hyp_weight = 0.1
a710e96583d5 adjust fudge factors
blanchet
parents: 41769
diff changeset
   905
val fact_min_weight = 0.2
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   906
val fact_max_weight = 1.0
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   907
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   908
fun add_term_weights weight (ATerm (s, tms)) =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   909
  (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   910
  #> fold (add_term_weights weight) tms
42538
9e3e45636459 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
blanchet
parents: 42534
diff changeset
   911
fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) =
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
   912
    formula_fold (add_term_weights weight) phi
42528
a15f0db2bcaf added support for TFF type declarations
blanchet
parents: 42527
diff changeset
   913
  | add_problem_line_weights _ _ = I
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   914
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   915
fun add_conjectures_weights [] = I
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   916
  | add_conjectures_weights conjs =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   917
    let val (hyps, conj) = split_last conjs in
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   918
      add_problem_line_weights conj_weight conj
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   919
      #> fold (add_problem_line_weights hyp_weight) hyps
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   920
    end
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   921
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   922
fun add_facts_weights facts =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   923
  let
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   924
    val num_facts = length facts
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   925
    fun weight_of j =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   926
      fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   927
                        / Real.fromInt num_facts
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   928
  in
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   929
    map weight_of (0 upto num_facts - 1) ~~ facts
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   930
    |> fold (uncurry add_problem_line_weights)
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   931
  end
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   932
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   933
(* Weights are from 0.0 (most important) to 1.0 (least important). *)
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   934
fun atp_problem_weights problem =
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   935
  Symtab.empty
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   936
  |> add_conjectures_weights (these (AList.lookup (op =) problem conjsN))
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   937
  |> add_facts_weights (these (AList.lookup (op =) problem factsN))
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   938
  |> Symtab.dest
41726
1ef01508bb9b sort E weights
blanchet
parents: 41491
diff changeset
   939
  |> sort (prod_ord Real.compare string_ord o pairself swap)
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   940
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   941
end;