src/HOL/Tools/ATP/atp_translate.ML
author blanchet
Wed, 01 Jun 2011 10:29:43 +0200
changeset 43136 cf5cda219058
parent 43130 d73fc2e55308
child 43139 9ed5d8ad8fa0
permissions -rw-r--r--
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
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
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
     9
signature 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
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43130
diff changeset
    12
  type connective = ATP_Problem.connective
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43130
diff changeset
    13
  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42895
diff changeset
    14
  type format = ATP_Problem.format
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
    15
  type formula_kind = ATP_Problem.formula_kind
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    16
  type 'a problem = 'a ATP_Problem.problem
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    17
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    18
  type name = string * string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    19
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    20
  datatype type_literal =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    21
    TyLitVar of name * name |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    22
    TyLitFree of name * name
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    23
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    24
  datatype arity_literal =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    25
    TConsLit of name * name * name list |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    26
    TVarLit of name * name
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    27
43086
blanchet
parents: 43085
diff changeset
    28
  type arity_clause =
blanchet
parents: 43085
diff changeset
    29
    {name: string,
blanchet
parents: 43085
diff changeset
    30
     prem_lits: arity_literal list,
blanchet
parents: 43085
diff changeset
    31
     concl_lits: arity_literal}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    32
43086
blanchet
parents: 43085
diff changeset
    33
  type class_rel_clause =
blanchet
parents: 43085
diff changeset
    34
    {name: string,
blanchet
parents: 43085
diff changeset
    35
     subclass: name,
blanchet
parents: 43085
diff changeset
    36
     superclass: name}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    37
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    38
  datatype combterm =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    39
    CombConst of name * typ * typ list |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    40
    CombVar of name * typ |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    41
    CombApp of combterm * combterm
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    42
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    43
  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    44
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    45
  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    46
  datatype type_level =
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    47
    All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
    48
  datatype type_heaviness = Heavyweight | Lightweight
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    49
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
    50
  datatype type_sys =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
    51
    Simple_Types of type_level |
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    52
    Preds of polymorphism * type_level * type_heaviness |
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    53
    Tags of polymorphism * type_level * type_heaviness
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    54
40114
blanchet
parents: 40069
diff changeset
    55
  type translated_formula
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    56
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    57
  val bound_var_prefix : string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    58
  val schematic_var_prefix: string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    59
  val fixed_var_prefix: string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    60
  val tvar_prefix: string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    61
  val tfree_prefix: string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    62
  val const_prefix: string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    63
  val type_const_prefix: string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    64
  val class_prefix: string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    65
  val skolem_const_prefix : string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    66
  val old_skolem_const_prefix : string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    67
  val new_skolem_const_prefix : string
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    68
  val type_decl_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    69
  val sym_decl_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    70
  val preds_sym_formula_prefix : string
43129
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    71
  val lightweight_tags_sym_formula_prefix : string
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
    72
  val fact_prefix : string
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    73
  val conjecture_prefix : string
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    74
  val helper_prefix : string
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    75
  val class_rel_clause_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    76
  val arity_clause_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    77
  val tfree_clause_prefix : string
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    78
  val typed_helper_suffix : string
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    79
  val untyped_helper_suffix : string
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    80
  val predicator_name : string
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    81
  val app_op_name : string
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43102
diff changeset
    82
  val type_tag_name : string
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    83
  val type_pred_name : string
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
    84
  val simple_type_prefix : string
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
    85
  val prefixed_app_op_name : string
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
    86
  val prefixed_type_tag_name : string
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    87
  val ascii_of: string -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    88
  val unascii_of: string -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    89
  val strip_prefix_and_unascii : string -> string -> string option
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    90
  val proxify_const : string -> (int * (string * string)) option
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    91
  val invert_const: string -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    92
  val unproxify_const: string -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    93
  val make_bound_var : string -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    94
  val make_schematic_var : string * int -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    95
  val make_fixed_var : string -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    96
  val make_schematic_type_var : string * int -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    97
  val make_fixed_type_var : string -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    98
  val make_fixed_const : string -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    99
  val make_fixed_type_const : string -> string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   100
  val make_type_class : string -> string
43093
blanchet
parents: 43092
diff changeset
   101
  val new_skolem_var_name_from_const : string -> string
blanchet
parents: 43092
diff changeset
   102
  val num_type_args : theory -> string -> int
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   103
  val make_arity_clauses :
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   104
    theory -> string list -> class list -> class list * arity_clause list
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   105
  val make_class_rel_clauses :
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   106
    theory -> class list -> class list -> class_rel_clause list
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   107
  val combtyp_of : combterm -> typ
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   108
  val strip_combterm_comb : combterm -> combterm * combterm list
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   109
  val atyps_of : typ -> typ list
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   110
  val combterm_from_term :
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   111
    theory -> (string * typ) list -> term -> combterm * typ list
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   112
  val is_locality_global : locality -> bool
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   113
  val type_sys_from_string : string -> type_sys
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   114
  val polymorphism_of_type_sys : type_sys -> polymorphism
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   115
  val level_of_type_sys : type_sys -> type_level
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   116
  val is_type_sys_virtually_sound : type_sys -> bool
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   117
  val is_type_sys_fairly_sound : type_sys -> bool
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   118
  val choose_format : format list -> type_sys -> format * type_sys
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   119
  val raw_type_literals_for_types : typ list -> type_literal list
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43130
diff changeset
   120
  val mk_aconns :
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43130
diff changeset
   121
    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
   122
  val unmangled_const_name : string -> string
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
   123
  val unmangled_const : string -> string * string fo_term list
41088
54eb8e7c7f9b clarified terminology
blanchet
parents: 40204
diff changeset
   124
  val translate_atp_fact :
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   125
    Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   126
    -> translated_formula option * ((string * locality) * thm)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   127
  val helper_table : (string * (bool * thm list)) list
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   128
  val tfree_classes_of_terms : term list -> string list
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   129
  val tvar_classes_of_terms : term list -> string list
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   130
  val type_consts_of_terms : theory -> term list -> string list
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39975
diff changeset
   131
  val prepare_atp_problem :
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   132
    Proof.context -> format -> formula_kind -> formula_kind -> type_sys
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   133
    -> bool option -> bool -> 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
   134
    -> (translated_formula option * ((string * 'a) * thm)) list
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
   135
    -> string problem * string Symtab.table * int * int
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   136
       * (string * 'a) list vector * int list * int Symtab.table
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   137
  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
   138
end;
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   139
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   140
structure ATP_Translate : ATP_TRANSLATE =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   141
struct
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   142
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   143
open ATP_Util
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   144
open ATP_Problem
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   145
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   146
type name = string * string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   147
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   148
(* FIXME: avoid *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   149
fun union_all xss = fold (union (op =)) xss []
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   150
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   151
(* experimental *)
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   152
val generate_useful_info = false
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   153
42879
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   154
fun useful_isabelle_info s =
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   155
  if generate_useful_info then
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   156
    SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   157
  else
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   158
    NONE
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   159
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   160
val intro_info = useful_isabelle_info "intro"
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   161
val elim_info = useful_isabelle_info "elim"
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   162
val simp_info = useful_isabelle_info "simp"
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   163
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   164
val bound_var_prefix = "B_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   165
val schematic_var_prefix = "V_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   166
val fixed_var_prefix = "v_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   167
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   168
val tvar_prefix = "T_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   169
val tfree_prefix = "t_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   170
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   171
val const_prefix = "c_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   172
val type_const_prefix = "tc_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   173
val class_prefix = "cl_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   174
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   175
val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   176
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   177
val new_skolem_const_prefix = skolem_const_prefix ^ "n"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   178
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   179
val type_decl_prefix = "ty_"
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   180
val sym_decl_prefix = "sy_"
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
   181
val preds_sym_formula_prefix = "psy_"
43129
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
   182
val lightweight_tags_sym_formula_prefix = "tsy_"
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
   183
val fact_prefix = "fact_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   184
val conjecture_prefix = "conj_"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   185
val helper_prefix = "help_"
43093
blanchet
parents: 43092
diff changeset
   186
val class_rel_clause_prefix = "crel_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   187
val arity_clause_prefix = "arity_"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   188
val tfree_clause_prefix = "tfree_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   189
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   190
val typed_helper_suffix = "_T"
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   191
val untyped_helper_suffix = "_U"
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   192
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   193
val predicator_name = "hBOOL"
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   194
val app_op_name = "hAPP"
43104
81d1b15aa0ae use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents: 43102
diff changeset
   195
val type_tag_name = "ti"
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   196
val type_pred_name = "is"
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   197
val simple_type_prefix = "ty_"
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   198
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
   199
val prefixed_app_op_name = const_prefix ^ app_op_name
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
   200
val prefixed_type_tag_name = const_prefix ^ type_tag_name
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
   201
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   202
(* Freshness almost guaranteed! *)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   203
val sledgehammer_weak_prefix = "Sledgehammer:"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   204
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   205
(*Escaping of special characters.
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   206
  Alphanumeric characters are left unchanged.
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   207
  The character _ goes to __
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   208
  Characters in the range ASCII space to / go to _A to _P, respectively.
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   209
  Other characters go to _nnn where nnn is the decimal ASCII code.*)
43093
blanchet
parents: 43092
diff changeset
   210
val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   211
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   212
fun stringN_of_int 0 _ = ""
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   213
  | stringN_of_int k n =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   214
    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   215
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   216
fun ascii_of_char c =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   217
  if Char.isAlphaNum c then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   218
    String.str c
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   219
  else if c = #"_" then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   220
    "__"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   221
  else if #" " <= c andalso c <= #"/" then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   222
    "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   223
  else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   224
    (* fixed width, in case more digits follow *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   225
    "_" ^ stringN_of_int 3 (Char.ord c)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   226
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   227
val ascii_of = String.translate ascii_of_char
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   228
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   229
(** Remove ASCII armoring from names in proof files **)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   230
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   231
(* We don't raise error exceptions because this code can run inside a worker
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   232
   thread. Also, the errors are impossible. *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   233
val unascii_of =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   234
  let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   235
    fun un rcs [] = String.implode(rev rcs)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   236
      | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   237
        (* Three types of _ escapes: __, _A to _P, _nnn *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   238
      | un rcs (#"_" :: #"_" :: cs) = un (#"_"::rcs) cs
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   239
      | un rcs (#"_" :: c :: cs) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   240
        if #"A" <= c andalso c<= #"P" then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   241
          (* translation of #" " to #"/" *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   242
          un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   243
        else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   244
          let val digits = List.take (c::cs, 3) handle Subscript => [] in
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   245
            case Int.fromString (String.implode digits) of
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   246
              SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   247
            | NONE => un (c:: #"_"::rcs) cs (* ERROR *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   248
          end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   249
      | un rcs (c :: cs) = un (c :: rcs) cs
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   250
  in un [] o String.explode end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   251
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   252
(* If string s has the prefix s1, return the result of deleting it,
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   253
   un-ASCII'd. *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   254
fun strip_prefix_and_unascii s1 s =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   255
  if String.isPrefix s1 s then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   256
    SOME (unascii_of (String.extract (s, size s1, NONE)))
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   257
  else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   258
    NONE
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   259
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   260
val proxies =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   261
  [("c_False",
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   262
    (@{const_name False}, (0, ("fFalse", @{const_name ATP.fFalse})))),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   263
   ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name ATP.fTrue})))),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   264
   ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name ATP.fNot})))),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   265
   ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name ATP.fconj})))),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   266
   ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name ATP.fdisj})))),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   267
   ("c_implies",
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   268
    (@{const_name implies}, (2, ("fimplies", @{const_name ATP.fimplies})))),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   269
   ("equal",
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   270
    (@{const_name HOL.eq}, (2, ("fequal", @{const_name ATP.fequal}))))]
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   271
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   272
val proxify_const = AList.lookup (op =) proxies #> Option.map snd
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   273
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   274
(* Readable names for the more common symbolic functions. Do not mess with the
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   275
   table unless you know what you are doing. *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   276
val const_trans_table =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   277
  [(@{type_name Product_Type.prod}, "prod"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   278
   (@{type_name Sum_Type.sum}, "sum"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   279
   (@{const_name False}, "False"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   280
   (@{const_name True}, "True"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   281
   (@{const_name Not}, "Not"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   282
   (@{const_name conj}, "conj"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   283
   (@{const_name disj}, "disj"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   284
   (@{const_name implies}, "implies"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   285
   (@{const_name HOL.eq}, "equal"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   286
   (@{const_name If}, "If"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   287
   (@{const_name Set.member}, "member"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   288
   (@{const_name Meson.COMBI}, "COMBI"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   289
   (@{const_name Meson.COMBK}, "COMBK"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   290
   (@{const_name Meson.COMBB}, "COMBB"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   291
   (@{const_name Meson.COMBC}, "COMBC"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   292
   (@{const_name Meson.COMBS}, "COMBS")]
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   293
  |> Symtab.make
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   294
  |> fold (Symtab.update o swap o snd o snd o snd) proxies
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   295
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   296
(* Invert the table of translations between Isabelle and ATPs. *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   297
val const_trans_table_inv =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   298
  const_trans_table |> Symtab.dest |> map swap |> Symtab.make
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   299
val const_trans_table_unprox =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   300
  Symtab.empty
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   301
  |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa)) proxies
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   302
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   303
val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   304
val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   305
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   306
fun lookup_const c =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   307
  case Symtab.lookup const_trans_table c of
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   308
    SOME c' => c'
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   309
  | NONE => ascii_of c
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   310
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   311
(*Remove the initial ' character from a type variable, if it is present*)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   312
fun trim_type_var s =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   313
  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   314
  else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   315
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   316
fun ascii_of_indexname (v,0) = ascii_of v
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   317
  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   318
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   319
fun make_bound_var x = bound_var_prefix ^ ascii_of x
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   320
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   321
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   322
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   323
fun make_schematic_type_var (x,i) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   324
      tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i))
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   325
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   326
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   327
(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   328
fun make_fixed_const @{const_name HOL.eq} = "equal"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   329
  | make_fixed_const c = const_prefix ^ lookup_const c
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   330
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   331
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   332
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   333
fun make_type_class clas = class_prefix ^ ascii_of clas
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   334
43093
blanchet
parents: 43092
diff changeset
   335
fun new_skolem_var_name_from_const s =
blanchet
parents: 43092
diff changeset
   336
  let val ss = s |> space_explode Long_Name.separator in
blanchet
parents: 43092
diff changeset
   337
    nth ss (length ss - 2)
blanchet
parents: 43092
diff changeset
   338
  end
blanchet
parents: 43092
diff changeset
   339
blanchet
parents: 43092
diff changeset
   340
(* The number of type arguments of a constant, zero if it's monomorphic. For
blanchet
parents: 43092
diff changeset
   341
   (instances of) Skolem pseudoconstants, this information is encoded in the
blanchet
parents: 43092
diff changeset
   342
   constant name. *)
blanchet
parents: 43092
diff changeset
   343
fun num_type_args thy s =
blanchet
parents: 43092
diff changeset
   344
  if String.isPrefix skolem_const_prefix s then
blanchet
parents: 43092
diff changeset
   345
    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
blanchet
parents: 43092
diff changeset
   346
  else
blanchet
parents: 43092
diff changeset
   347
    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
blanchet
parents: 43092
diff changeset
   348
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   349
(** Definitions and functions for FOL clauses and formulas for TPTP **)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   350
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   351
(* The first component is the type class; the second is a "TVar" or "TFree". *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   352
datatype type_literal =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   353
  TyLitVar of name * name |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   354
  TyLitFree of name * name
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   355
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   356
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   357
(** Isabelle arities **)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   358
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   359
datatype arity_literal =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   360
  TConsLit of name * name * name list |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   361
  TVarLit of name * name
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   362
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   363
fun gen_TVars 0 = []
43093
blanchet
parents: 43092
diff changeset
   364
  | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   365
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   366
fun pack_sort (_,[])  = []
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   367
  | pack_sort (tvar, "HOL.type" :: srt) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   368
    pack_sort (tvar, srt) (* IGNORE sort "type" *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   369
  | pack_sort (tvar, cls :: srt) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   370
    (`make_type_class cls, `I tvar) :: pack_sort (tvar, srt)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   371
43086
blanchet
parents: 43085
diff changeset
   372
type arity_clause =
blanchet
parents: 43085
diff changeset
   373
  {name: string,
blanchet
parents: 43085
diff changeset
   374
   prem_lits: arity_literal list,
blanchet
parents: 43085
diff changeset
   375
   concl_lits: arity_literal}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   376
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   377
(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   378
fun make_axiom_arity_clause (tcons, name, (cls, args)) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   379
  let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   380
    val tvars = gen_TVars (length args)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   381
    val tvars_srts = ListPair.zip (tvars, args)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   382
  in
43086
blanchet
parents: 43085
diff changeset
   383
    {name = name,
blanchet
parents: 43085
diff changeset
   384
     prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)),
blanchet
parents: 43085
diff changeset
   385
     concl_lits = TConsLit (`make_type_class cls,
blanchet
parents: 43085
diff changeset
   386
                            `make_fixed_type_const tcons,
blanchet
parents: 43085
diff changeset
   387
                            tvars ~~ tvars)}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   388
  end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   389
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   390
fun arity_clause _ _ (_, []) = []
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   391
  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   392
      arity_clause seen n (tcons,ars)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   393
  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   394
      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   395
          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) ::
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   396
          arity_clause seen (n+1) (tcons,ars)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   397
      else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   398
          make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   399
          arity_clause (class::seen) n (tcons,ars)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   400
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   401
fun multi_arity_clause [] = []
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   402
  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   403
      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   404
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   405
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   406
  provided its arguments have the corresponding sorts.*)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   407
fun type_class_pairs thy tycons classes =
43093
blanchet
parents: 43092
diff changeset
   408
  let
blanchet
parents: 43092
diff changeset
   409
    val alg = Sign.classes_of thy
blanchet
parents: 43092
diff changeset
   410
    fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
blanchet
parents: 43092
diff changeset
   411
    fun add_class tycon class =
blanchet
parents: 43092
diff changeset
   412
      cons (class, domain_sorts tycon class)
blanchet
parents: 43092
diff changeset
   413
      handle Sorts.CLASS_ERROR _ => I
blanchet
parents: 43092
diff changeset
   414
    fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
blanchet
parents: 43092
diff changeset
   415
  in map try_classes tycons end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   416
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   417
(*Proving one (tycon, class) membership may require proving others, so iterate.*)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   418
fun iter_type_class_pairs _ _ [] = ([], [])
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   419
  | iter_type_class_pairs thy tycons classes =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   420
      let val cpairs = type_class_pairs thy tycons classes
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   421
          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   422
            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   423
          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
43093
blanchet
parents: 43092
diff changeset
   424
      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   425
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   426
fun make_arity_clauses thy tycons =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   427
  iter_type_class_pairs thy tycons ##> multi_arity_clause
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   428
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   429
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   430
(** Isabelle class relations **)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   431
43086
blanchet
parents: 43085
diff changeset
   432
type class_rel_clause =
blanchet
parents: 43085
diff changeset
   433
  {name: string,
blanchet
parents: 43085
diff changeset
   434
   subclass: name,
blanchet
parents: 43085
diff changeset
   435
   superclass: name}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   436
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   437
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   438
fun class_pairs _ [] _ = []
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   439
  | class_pairs thy subs supers =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   440
      let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   441
        val class_less = Sorts.class_less (Sign.classes_of thy)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   442
        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   443
        fun add_supers sub = fold (add_super sub) supers
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   444
      in fold add_supers subs [] end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   445
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   446
fun make_class_rel_clause (sub,super) =
43086
blanchet
parents: 43085
diff changeset
   447
  {name = sub ^ "_" ^ super,
blanchet
parents: 43085
diff changeset
   448
   subclass = `make_type_class sub,
blanchet
parents: 43085
diff changeset
   449
   superclass = `make_type_class super}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   450
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   451
fun make_class_rel_clauses thy subs supers =
43093
blanchet
parents: 43092
diff changeset
   452
  map make_class_rel_clause (class_pairs thy subs supers)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   453
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   454
datatype combterm =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   455
  CombConst of name * typ * typ list |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   456
  CombVar of name * typ |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   457
  CombApp of combterm * combterm
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   458
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   459
fun combtyp_of (CombConst (_, T, _)) = T
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   460
  | combtyp_of (CombVar (_, T)) = T
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   461
  | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   462
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   463
(*gets the head of a combinator application, along with the list of arguments*)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   464
fun strip_combterm_comb u =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   465
    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   466
        |   stripc  x =  x
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   467
    in stripc(u,[]) end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   468
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   469
fun atyps_of T = fold_atyps (insert (op =)) T []
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   470
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   471
fun new_skolem_const_name s num_T_args =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   472
  [new_skolem_const_prefix, s, string_of_int num_T_args]
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   473
  |> space_implode Long_Name.separator
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   474
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   475
(* Converts a term (with combinators) into a combterm. Also accumulates sort
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   476
   infomation. *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   477
fun combterm_from_term thy bs (P $ Q) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   478
    let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   479
      val (P', P_atomics_Ts) = combterm_from_term thy bs P
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   480
      val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   481
    in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   482
  | combterm_from_term thy _ (Const (c, T)) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   483
    let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   484
      val tvar_list =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   485
        (if String.isPrefix old_skolem_const_prefix c then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   486
           [] |> Term.add_tvarsT T |> map TVar
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   487
         else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   488
           (c, T) |> Sign.const_typargs thy)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   489
      val c' = CombConst (`make_fixed_const c, T, tvar_list)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   490
    in (c', atyps_of T) end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   491
  | combterm_from_term _ _ (Free (v, T)) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   492
    (CombConst (`make_fixed_var v, T, []), atyps_of T)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   493
  | combterm_from_term _ _ (Var (v as (s, _), T)) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   494
    (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   495
       let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   496
         val Ts = T |> strip_type |> swap |> op ::
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   497
         val s' = new_skolem_const_name s (length Ts)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   498
       in CombConst (`make_fixed_const s', T, Ts) end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   499
     else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   500
       CombVar ((make_schematic_var v, s), T), atyps_of T)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   501
  | combterm_from_term _ bs (Bound j) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   502
    nth bs j
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   503
    |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   504
  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   505
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   506
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   507
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   508
(* (quasi-)underapproximation of the truth *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   509
fun is_locality_global Local = false
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   510
  | is_locality_global Assum = false
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   511
  | is_locality_global Chained = false
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   512
  | is_locality_global _ = true
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   513
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   514
datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   515
datatype type_level =
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   516
  All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   517
datatype type_heaviness = Heavyweight | Lightweight
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   518
43102
9a42899ec169 tuned name
blanchet
parents: 43101
diff changeset
   519
datatype type_sys =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   520
  Simple_Types of type_level |
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   521
  Preds of polymorphism * type_level * type_heaviness |
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   522
  Tags of polymorphism * type_level * type_heaviness
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   523
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   524
fun try_unsuffixes ss s =
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   525
  fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   526
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   527
fun type_sys_from_string s =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   528
  (case try (unprefix "poly_") s of
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   529
     SOME s => (SOME Polymorphic, s)
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   530
   | NONE =>
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   531
     case try (unprefix "mono_") s of
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   532
       SOME s => (SOME Monomorphic, s)
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   533
     | NONE =>
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   534
       case try (unprefix "mangled_") s of
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   535
         SOME s => (SOME Mangled_Monomorphic, s)
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   536
       | NONE => (NONE, s))
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   537
  ||> (fn s =>
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   538
          (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   539
          case try_unsuffixes ["?", "_query"] s of
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   540
            SOME s => (Nonmonotonic_Types, s)
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   541
          | NONE =>
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   542
            case try_unsuffixes ["!", "_bang"] s of
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   543
              SOME s => (Finite_Types, s)
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   544
            | NONE => (All_Types, s))
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   545
  ||> apsnd (fn s =>
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   546
                case try (unsuffix "_heavy") s of
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   547
                  SOME s => (Heavyweight, s)
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   548
                | NONE => (Lightweight, s))
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   549
  |> (fn (poly, (level, (heaviness, core))) =>
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   550
         case (core, (poly, level, heaviness)) of
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   551
           ("simple", (NONE, _, Lightweight)) => Simple_Types level
42854
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   552
         | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
42851
3bb63850488b removed "poly_tags_light_bang" since highly unsound
blanchet
parents: 42837
diff changeset
   553
         | ("tags", (SOME Polymorphic, All_Types, _)) =>
42854
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   554
           Tags (Polymorphic, All_Types, heaviness)
42886
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   555
         | ("tags", (SOME Polymorphic, _, _)) =>
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   556
           (* The actual light encoding is very unsound. *)
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   557
           Tags (Polymorphic, level, Heavyweight)
42854
d99167ac4f8a since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents: 42852
diff changeset
   558
         | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   559
         | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   560
           Preds (poly, Const_Arg_Types, Lightweight)
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   561
         | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   562
           Preds (Polymorphic, No_Types, Lightweight)
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   563
         | _ => raise Same.SAME)
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   564
  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   565
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   566
fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   567
  | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   568
  | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   569
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   570
fun level_of_type_sys (Simple_Types level) = level
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   571
  | level_of_type_sys (Preds (_, level, _)) = level
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   572
  | level_of_type_sys (Tags (_, level, _)) = level
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   573
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   574
fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   575
  | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   576
  | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   577
42687
blanchet
parents: 42685
diff changeset
   578
fun is_type_level_virtually_sound level =
blanchet
parents: 42685
diff changeset
   579
  level = All_Types orelse level = Nonmonotonic_Types
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   580
val is_type_sys_virtually_sound =
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   581
  is_type_level_virtually_sound o level_of_type_sys
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   582
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   583
fun is_type_level_fairly_sound level =
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   584
  is_type_level_virtually_sound level orelse level = Finite_Types
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   585
val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   586
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   587
fun is_setting_higher_order THF (Simple_Types _) = true
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   588
  | is_setting_higher_order _ _ = false
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   589
43101
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   590
fun choose_format formats (Simple_Types level) =
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   591
    if member (op =) formats THF then (THF, Simple_Types level)
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   592
    else if member (op =) formats TFF then (TFF, Simple_Types level)
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   593
    else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
43101
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   594
  | choose_format formats type_sys =
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   595
    (case hd formats of
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   596
       CNF_UEQ =>
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   597
       (CNF_UEQ, case type_sys of
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   598
                   Preds stuff =>
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   599
                   (if is_type_sys_fairly_sound type_sys then Preds else Tags)
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   600
                       stuff
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   601
                 | _ => type_sys)
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   602
     | format => (format, type_sys))
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   603
40114
blanchet
parents: 40069
diff changeset
   604
type translated_formula =
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38748
diff changeset
   605
  {name: string,
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   606
   locality: locality,
42525
7a506b0b644f distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree
blanchet
parents: 42524
diff changeset
   607
   kind: formula_kind,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   608
   combformula: (name, typ, combterm) formula,
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   609
   atomic_types: typ list}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   610
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   611
fun update_combformula f ({name, locality, kind, combformula, atomic_types}
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   612
                          : translated_formula) =
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   613
  {name = name, locality = locality, kind = kind, combformula = f combformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   614
   atomic_types = atomic_types} : translated_formula
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   615
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   616
fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
   617
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   618
val type_instance = Sign.typ_instance o Proof_Context.theory_of
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   619
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   620
fun insert_type ctxt get_T x xs =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   621
  let val T = get_T x in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   622
    if exists (curry (type_instance ctxt) T o get_T) xs then xs
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   623
    else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   624
  end
42677
25496cd3c199 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
blanchet
parents: 42675
diff changeset
   625
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   626
(* The Booleans indicate whether all type arguments should be kept. *)
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   627
datatype type_arg_policy =
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   628
  Explicit_Type_Args of bool |
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   629
  Mangled_Type_Args of bool |
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   630
  No_Type_Args
41136
30bedf58b177 implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents: 41134
diff changeset
   631
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   632
fun should_drop_arg_type_args (Simple_Types _) =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   633
    false (* since TFF doesn't support overloading *)
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   634
  | should_drop_arg_type_args type_sys =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   635
    level_of_type_sys type_sys = All_Types andalso
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   636
    heaviness_of_type_sys type_sys = Heavyweight
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   637
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   638
fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
43105
bb0ceef7d39f no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents: 43104
diff changeset
   639
  | general_type_arg_policy type_sys =
bb0ceef7d39f no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents: 43104
diff changeset
   640
    if level_of_type_sys type_sys = No_Types then
bb0ceef7d39f no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents: 43104
diff changeset
   641
      No_Type_Args
bb0ceef7d39f no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents: 43104
diff changeset
   642
    else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
bb0ceef7d39f no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents: 43104
diff changeset
   643
      Mangled_Type_Args (should_drop_arg_type_args type_sys)
bb0ceef7d39f no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents: 43104
diff changeset
   644
    else
bb0ceef7d39f no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents: 43104
diff changeset
   645
      Explicit_Type_Args (should_drop_arg_type_args type_sys)
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   646
42951
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   647
fun type_arg_policy type_sys s =
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   648
  if s = @{const_name HOL.eq} orelse
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   649
     (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
42951
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   650
    No_Type_Args
43105
bb0ceef7d39f no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents: 43104
diff changeset
   651
  else if s = type_tag_name then
bb0ceef7d39f no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents: 43104
diff changeset
   652
    Explicit_Type_Args false
42951
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   653
  else
40bf0173fbed pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents: 42944
diff changeset
   654
    general_type_arg_policy type_sys
42227
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 42180
diff changeset
   655
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   656
(*Make literals for sorted type variables*)
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   657
fun generic_sorts_on_type (_, []) = []
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   658
  | generic_sorts_on_type ((x, i), s :: ss) =
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   659
    generic_sorts_on_type ((x, i), ss)
43093
blanchet
parents: 43092
diff changeset
   660
    |> (if s = the_single @{sort HOL.type} then
blanchet
parents: 43092
diff changeset
   661
          I
blanchet
parents: 43092
diff changeset
   662
        else if i = ~1 then
blanchet
parents: 43092
diff changeset
   663
          cons (TyLitFree (`make_type_class s, `make_fixed_type_var x))
blanchet
parents: 43092
diff changeset
   664
        else
blanchet
parents: 43092
diff changeset
   665
          cons (TyLitVar (`make_type_class s,
blanchet
parents: 43092
diff changeset
   666
                          (make_schematic_type_var (x, i), x))))
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   667
fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   668
  | sorts_on_tfree _ = []
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   669
fun sorts_on_tvar (TVar z) = generic_sorts_on_type z
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   670
  | sorts_on_tvar _ = []
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   671
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   672
(* Given a list of sorted type variables, return a list of type literals. *)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   673
fun raw_type_literals_for_types Ts =
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   674
  union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   675
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   676
fun type_literals_for_types type_sys sorts_on_typ Ts =
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   677
  if level_of_type_sys type_sys = No_Types then []
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   678
  else union_all (map sorts_on_typ Ts)
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
   679
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
   680
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
   681
  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
   682
    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
   683
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   684
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
   685
  | 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
   686
fun mk_aquant _ [] phi = phi
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   687
  | 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
   688
    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
   689
  | 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
   690
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   691
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
   692
  let
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   693
    fun formula_vars bounds (AQuant (_, xs, phi)) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   694
        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
   695
      | 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
   696
      | formula_vars bounds (AAtom tm) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   697
        union (op =) (atom_vars tm []
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   698
                      |> 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
   699
  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
   700
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   701
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
   702
  | combterm_vars (CombConst _) = I
42574
blanchet
parents: 42573
diff changeset
   703
  | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   704
fun close_combformula_universally phi = close_universally combterm_vars phi
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   705
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   706
fun term_vars (ATerm (name as (s, _), tms)) =
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   707
  is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
42674
af86324707f2 eta-expansion for SML/NJ
blanchet
parents: 42670
diff changeset
   708
fun close_formula_universally phi = close_universally term_vars phi
41145
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   709
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   710
val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   711
val homo_infinite_type = Type (homo_infinite_type_name, [])
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   712
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   713
fun fo_term_from_typ higher_order =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   714
  let
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   715
    fun term (Type (s, Ts)) =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   716
      ATerm (case (higher_order, s) of
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   717
               (true, @{type_name bool}) => `I tptp_bool_type
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   718
             | (true, @{type_name fun}) => `I tptp_fun_type
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   719
             | _ => if s = homo_infinite_type_name then `I tptp_individual_type
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   720
                    else `make_fixed_type_const s,
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   721
             map term Ts)
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   722
    | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   723
    | term (TVar ((x as (s, _)), _)) =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   724
      ATerm ((make_schematic_type_var x, s), [])
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   725
  in term end
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   726
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   727
(* This shouldn't clash with anything else. *)
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   728
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
   729
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   730
fun generic_mangled_type_name f (ATerm (name, [])) = f name
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   731
  | generic_mangled_type_name f (ATerm (name, tys)) =
42761
8ea9c6fa8b53 fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
blanchet
parents: 42755
diff changeset
   732
    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
8ea9c6fa8b53 fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
blanchet
parents: 42755
diff changeset
   733
    ^ ")"
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
   734
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   735
val bool_atype = AType (`I tptp_bool_type)
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   736
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   737
fun make_simple_type s =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   738
  if s = tptp_bool_type orelse s = tptp_fun_type orelse
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   739
     s = tptp_individual_type then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   740
    s
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   741
  else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   742
    simple_type_prefix ^ ascii_of s
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   743
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   744
fun ho_type_from_fo_term higher_order pred_sym ary =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   745
  let
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   746
    fun to_atype ty =
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   747
      AType ((make_simple_type (generic_mangled_type_name fst ty),
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   748
              generic_mangled_type_name snd ty))
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   749
    fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   750
    fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   751
      | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   752
    fun to_ho (ty as ATerm ((s, _), tys)) =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   753
      if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   754
  in if higher_order then to_ho else to_fo ary end
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   755
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   756
fun mangled_type higher_order pred_sym ary =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   757
  ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   758
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   759
fun mangled_const_name T_args (s, s') =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   760
  let
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   761
    val ty_args = map (fo_term_from_typ false) T_args
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   762
    fun type_suffix f g =
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   763
      fold_rev (curry (op ^) o g o prefix mangled_type_sep
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   764
                o generic_mangled_type_name f) ty_args ""
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   765
  in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   766
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
   767
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
   768
  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
   769
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
   770
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
   771
  (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
   772
   -- 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
   773
                    [] >> 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
   774
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
   775
  (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
   776
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
   777
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
   778
  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
   779
    |> 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
   780
           (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
   781
                                                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
   782
    |> 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
   783
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   784
val unmangled_const_name = space_explode mangled_type_sep #> hd
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
   785
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
   786
  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
   787
    (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
   788
  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
   789
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   790
fun introduce_proxies format type_sys =
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   791
  let
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   792
    fun intro top_level (CombApp (tm1, tm2)) =
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   793
        CombApp (intro top_level tm1, intro false tm2)
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   794
      | intro top_level (CombConst (name as (s, _), T, T_args)) =
42570
77f94ac04f32 cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents: 42569
diff changeset
   795
        (case proxify_const s of
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   796
           SOME (_, proxy_base) =>
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   797
           if top_level orelse is_setting_higher_order format type_sys then
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   798
             case (top_level, s) of
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   799
               (_, "c_False") => (`I tptp_false, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   800
             | (_, "c_True") => (`I tptp_true, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   801
             | (false, "c_Not") => (`I tptp_not, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   802
             | (false, "c_conj") => (`I tptp_and, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   803
             | (false, "c_disj") => (`I tptp_or, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   804
             | (false, "c_implies") => (`I tptp_implies, [])
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   805
             | (false, s) =>
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   806
               if is_tptp_equal s then (`I tptp_equal, [])
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   807
               else (proxy_base |>> prefix const_prefix, T_args)
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   808
             | _ => (name, [])
42569
5737947e4c77 make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents: 42568
diff changeset
   809
           else
42574
blanchet
parents: 42573
diff changeset
   810
             (proxy_base |>> prefix const_prefix, T_args)
blanchet
parents: 42573
diff changeset
   811
          | NONE => (name, T_args))
blanchet
parents: 42573
diff changeset
   812
        |> (fn (name, T_args) => CombConst (name, T, T_args))
43017
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   813
      | intro _ tm = tm
944b19ab6003 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents: 43001
diff changeset
   814
  in intro true end
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   815
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   816
fun combformula_from_prop thy format type_sys eq_as_iff =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   817
  let
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   818
    fun do_term bs t atomic_types =
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   819
      combterm_from_term thy bs (Envir.eta_contract t)
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   820
      |>> (introduce_proxies format type_sys #> AAtom)
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   821
      ||> union (op =) atomic_types
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   822
    fun do_quant bs q s T t' =
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   823
      let val s = Name.variant (map fst bs) s in
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   824
        do_formula ((s, T) :: bs) t'
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   825
        #>> mk_aquant q [(`make_bound_var s, SOME T)]
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   826
      end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   827
    and do_conn bs c t1 t2 =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   828
      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
   829
      #>> uncurry (mk_aconn c)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   830
    and do_formula bs t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   831
      case t of
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   832
        @{const Trueprop} $ t1 => do_formula bs t1
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   833
      | @{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
   834
      | 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
   835
        do_quant bs AForall s T t'
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   836
      | 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
   837
        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
   838
      | @{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
   839
      | @{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
   840
      | @{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
   841
      | 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
   842
        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
   843
      | _ => do_term bs t
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   844
  in do_formula [] end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   845
42750
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   846
fun presimplify_term ctxt =
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   847
  Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   848
  #> Meson.presimplify ctxt
c8b1d9ee3758 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents: 42747
diff changeset
   849
  #> prop_of
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   850
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41406
diff changeset
   851
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
   852
fun conceal_bounds Ts t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   853
  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
   854
                    (0 upto length Ts - 1 ~~ Ts), t)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   855
fun reveal_bounds Ts =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   856
  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
   857
                    (0 upto length Ts - 1 ~~ Ts))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   858
42747
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   859
fun extensionalize_term ctxt t =
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   860
  let val thy = Proof_Context.theory_of ctxt in
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   861
    t |> cterm_of thy |> Meson.extensionalize_conv ctxt
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   862
      |> prop_of |> Logic.dest_equals |> snd
f132d13fcf75 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents: 42742
diff changeset
   863
  end
38608
01ed56c46259 beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents: 38606
diff changeset
   864
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   865
fun introduce_combinators_in_term ctxt kind t =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   866
  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
   867
    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
   868
      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
   869
    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
   870
      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
   871
        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
   872
          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
   873
            @{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
   874
          | (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
   875
            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
   876
          | (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
   877
            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
   878
          | (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
   879
            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
   880
          | (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
   881
            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
   882
          | (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
   883
          | (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
   884
          | (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
   885
          | (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
   886
              $ 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
   887
            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
   888
          | _ => 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
   889
                   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
   890
                 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
   891
                   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
   892
                     |> 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
   893
                     |> cterm_of thy
39890
a1695e2169d0 finished renaming file and module
blanchet
parents: 39886
diff changeset
   894
                     |> 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
   895
                     |> 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
   896
                     |> reveal_bounds Ts
39370
f8292d3020db use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents: 39005
diff changeset
   897
        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
   898
      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
   899
      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
   900
             (* 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
   901
             if kind = Conjecture then HOLogic.false_const
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   902
             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
   903
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   904
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   905
(* 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
   906
   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
   907
fun freeze_term t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   908
  let
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   909
    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
   910
      | 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
   911
      | aux (Var ((s, i), T)) =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   912
        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
   913
      | aux t = t
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   914
  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
   915
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   916
fun preprocess_prop ctxt presimp kind t =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   917
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   918
    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
   919
    val t = t |> Envir.beta_eta_contract
42944
9e620869a576 improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents: 42943
diff changeset
   920
              |> transform_elim_prop
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41199
diff changeset
   921
              |> Object_Logic.atomize_term thy
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   922
    val need_trueprop = (fastype_of t = @{typ bool})
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   923
  in
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   924
    t |> need_trueprop ? HOLogic.mk_Trueprop
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   925
      |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   926
      |> extensionalize_term ctxt
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   927
      |> presimp ? presimplify_term ctxt
43120
a9c2cdf4ae97 make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
blanchet
parents: 43105
diff changeset
   928
      |> perhaps (try (HOLogic.dest_Trueprop))
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   929
      |> introduce_combinators_in_term ctxt kind
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   930
  end
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   931
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   932
(* making fact and conjecture formulas *)
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   933
fun make_formula thy format type_sys eq_as_iff name loc kind t =
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   934
  let
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   935
    val (combformula, atomic_types) =
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   936
      combformula_from_prop thy format type_sys eq_as_iff t []
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   937
  in
42640
879d2d6b05ce generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents: 42613
diff changeset
   938
    {name = name, locality = loc, kind = kind, combformula = combformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   939
     atomic_types = atomic_types}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   940
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   941
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   942
fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   943
              ((name, loc), t) =
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   944
  let val thy = Proof_Context.theory_of ctxt in
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   945
    case (keep_trivial,
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   946
          t |> preproc ? preprocess_prop ctxt presimp Axiom
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   947
            |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   948
      (false,
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   949
       formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   950
      if s = tptp_true then NONE else SOME formula
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   951
    | (_, formula) => SOME formula
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   952
  end
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   953
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   954
fun make_conjecture ctxt format prem_kind type_sys preproc ts =
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   955
  let
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   956
    val thy = Proof_Context.theory_of ctxt
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   957
    val last = length ts - 1
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   958
  in
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   959
    map2 (fn j => fn t =>
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   960
             let
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   961
               val (kind, maybe_negate) =
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   962
                 if j = last then
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   963
                   (Conjecture, I)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   964
                 else
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   965
                   (prem_kind,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   966
                    if prem_kind = Conjecture then update_combformula mk_anot
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   967
                    else I)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   968
              in
43098
e88e974c4846 proper handling of type variable classes in new Metis
blanchet
parents: 43096
diff changeset
   969
                t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   970
                  |> make_formula thy format type_sys true (string_of_int j)
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   971
                                  General kind
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   972
                  |> maybe_negate
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42701
diff changeset
   973
              end)
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   974
         (0 upto last) ts
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
   975
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   976
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   977
(** Finite and infinite type inference **)
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   978
42886
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   979
fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   980
  | deep_freeze_atyp T = T
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   981
val deep_freeze_type = map_atyps deep_freeze_atyp
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   982
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   983
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   984
   dangerous because their "exhaust" properties can easily lead to unsound ATP
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   985
   proofs. On the other hand, all HOL infinite types can be given the same
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   986
   models in first-order logic (via Löwenheim-Skolem). *)
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   987
42886
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   988
fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
208ec29cc013 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents: 42885
diff changeset
   989
    exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   990
  | should_encode_type _ _ All_Types _ = true
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   991
  | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   992
  | should_encode_type _ _ _ _ = false
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   993
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   994
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   995
                             should_predicate_on_var T =
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   996
    (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
42878
85ac4c12a4b7 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents: 42855
diff changeset
   997
    should_encode_type ctxt nonmono_Ts level T
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
   998
  | should_predicate_on_type _ _ _ _ _ = false
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
   999
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1000
fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1001
    String.isPrefix bound_var_prefix s
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1002
  | is_var_or_bound_var (CombVar _) = true
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1003
  | is_var_or_bound_var _ = false
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1004
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1005
datatype tag_site = Top_Level | Eq_Arg | Elsewhere
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1006
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1007
fun should_tag_with_type _ _ _ Top_Level _ _ = false
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
  1008
  | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T =
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
  1009
    (case heaviness of
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
  1010
       Heavyweight => should_encode_type ctxt nonmono_Ts level T
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
  1011
     | Lightweight =>
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1012
       case (site, is_var_or_bound_var u) of
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1013
         (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1014
       | _ => false)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1015
  | should_tag_with_type _ _ _ _ _ _ = false
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
  1016
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1017
fun homogenized_type ctxt nonmono_Ts level =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1018
  let
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1019
    val should_encode = should_encode_type ctxt nonmono_Ts level
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1020
    fun homo 0 T = if should_encode T then T else homo_infinite_type
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1021
      | homo ary (Type (@{type_name fun}, [T1, T2])) =
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1022
        homo 0 T1 --> homo (ary - 1) T2
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1023
      | homo _ _ = raise Fail "expected function type"
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1024
  in homo end
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
  1025
42573
744215c3e90c got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents: 42572
diff changeset
  1026
(** "hBOOL" and "hAPP" **)
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1027
42574
blanchet
parents: 42573
diff changeset
  1028
type sym_info =
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1029
  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
  1030
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1031
fun add_combterm_syms_to_table ctxt explicit_apply =
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1032
  let
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1033
    fun consider_var_arity const_T var_T max_ary =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1034
      let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1035
        fun iter ary T =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1036
          if ary = max_ary orelse type_instance ctxt (var_T, T) then ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1037
          else iter (ary + 1) (range_type T)
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1038
      in iter 0 const_T end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1039
    fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1040
      let val (head, args) = strip_combterm_comb tm in
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1041
        (case head of
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
  1042
           CombConst ((s, _), T, _) =>
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1043
           if String.isPrefix bound_var_prefix s then
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1044
             if explicit_apply = NONE andalso can dest_funT T then
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1045
               let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1046
                 fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1047
                   {pred_sym = pred_sym,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1048
                    min_ary =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1049
                      fold (fn T' => consider_var_arity T' T) types min_ary,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1050
                    max_ary = max_ary, types = types}
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1051
                 val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1052
               in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1053
                 if pointer_eq (ho_var_Ts', ho_var_Ts) then accum
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1054
                 else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1055
               end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1056
             else
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1057
               accum
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1058
           else
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1059
             let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1060
               val ary = length args
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1061
             in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1062
               (ho_var_Ts,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1063
                case Symtab.lookup sym_tab s of
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1064
                  SOME {pred_sym, min_ary, max_ary, types} =>
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1065
                  let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1066
                    val types' = types |> insert_type ctxt I T
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1067
                    val min_ary =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1068
                      if is_some explicit_apply orelse
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1069
                         pointer_eq (types', types) then
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1070
                        min_ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1071
                      else
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1072
                        fold (consider_var_arity T) ho_var_Ts min_ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1073
                  in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1074
                    Symtab.update (s, {pred_sym = pred_sym andalso top_level,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1075
                                       min_ary = Int.min (ary, min_ary),
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1076
                                       max_ary = Int.max (ary, max_ary),
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1077
                                       types = types'})
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1078
                                  sym_tab
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1079
                  end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1080
                | NONE =>
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1081
                  let
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1082
                    val min_ary =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1083
                      case explicit_apply of
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1084
                        SOME true => 0
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1085
                      | SOME false => ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1086
                      | NONE => fold (consider_var_arity T) ho_var_Ts ary
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1087
                  in
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1088
                    Symtab.update_new (s, {pred_sym = top_level,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1089
                                           min_ary = min_ary, max_ary = ary,
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1090
                                           types = [T]})
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1091
                                      sym_tab
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1092
                  end)
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1093
             end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1094
         | _ => accum)
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1095
        |> fold (add false) args
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1096
      end
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1097
  in add true end
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1098
fun add_fact_syms_to_table ctxt explicit_apply =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1099
  fact_lift (formula_fold NONE
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1100
                          (K (add_combterm_syms_to_table ctxt explicit_apply)))
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1101
42675
223153bb68a1 added type annotation for SML/NJ
blanchet
parents: 42674
diff changeset
  1102
val default_sym_table_entries : (string * sym_info) list =
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1103
  [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1104
   (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
  1105
   (make_fixed_const predicator_name,
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1106
    {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
  1107
  ([tptp_false, tptp_true]
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1108
   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
  1109
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1110
fun sym_table_for_facts ctxt explicit_apply facts =
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1111
  Symtab.empty
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1112
  |> fold Symtab.default default_sym_table_entries
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1113
  |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1114
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1115
fun min_arity_of sym_tab s =
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1116
  case Symtab.lookup sym_tab s of
42574
blanchet
parents: 42573
diff changeset
  1117
    SOME ({min_ary, ...} : sym_info) => min_ary
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1118
  | NONE =>
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1119
    case strip_prefix_and_unascii const_prefix s of
42547
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
  1120
      SOME s =>
42570
77f94ac04f32 cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents: 42569
diff changeset
  1121
      let val s = s |> unmangled_const_name |> invert_const in
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
  1122
        if s = predicator_name then 1
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
  1123
        else if s = app_op_name then 2
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
  1124
        else if s = type_pred_name then 1
42557
ae0deb39a254 fixed min-arity computation when "explicit_apply" is specified
blanchet
parents: 42556
diff changeset
  1125
        else 0
42547
b5eec0c99528 fixed arity of special constants if "explicit_apply" is set
blanchet
parents: 42546
diff changeset
  1126
      end
42544
75cb06eee990 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents: 42543
diff changeset
  1127
    | NONE => 0
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1128
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1129
(* 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
  1130
   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
  1131
   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
  1132
   arguments and is used as a predicate. *)
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1133
fun is_pred_sym sym_tab s =
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1134
  case Symtab.lookup sym_tab s of
42574
blanchet
parents: 42573
diff changeset
  1135
    SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
blanchet
parents: 42573
diff changeset
  1136
    pred_sym andalso min_ary = max_ary
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1137
  | NONE => false
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1138
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
  1139
val predicator_combconst =
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
  1140
  CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
  1141
fun predicator tm = CombApp (predicator_combconst, tm)
42542
024920b65ce2 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents: 42541
diff changeset
  1142