src/HOL/Tools/ATP/atp_translate.ML
author blanchet
Thu, 28 Jul 2011 11:43:45 +0200
changeset 43997 578460971517
parent 43989 eb763b3ff9ed
child 44001 2b75760fa75e
permissions -rw-r--r--
fixed lambda concealing
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43283
446e6621762d updated headers;
wenzelm
parents: 43278
diff changeset
     1
(*  Title:      HOL/Tools/ATP/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
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
     6
Translation of HOL to FOL for Metis and 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
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
    11
  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_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
43421
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43401
diff changeset
    18
  datatype locality =
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43401
diff changeset
    19
    General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43401
diff changeset
    20
    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
    21
43624
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
    22
  datatype order = First_Order | Higher_Order
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
    23
  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
    24
  datatype type_level =
43362
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
    25
    All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
    26
    No_Types
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
    27
  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
    28
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    29
  datatype type_enc =
43624
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
    30
    Simple_Types of order * type_level |
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
    31
    Guards of polymorphism * type_level * type_heaviness |
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
    32
    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
    33
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    34
  val bound_var_prefix : string
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    35
  val schematic_var_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    36
  val fixed_var_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    37
  val tvar_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    38
  val tfree_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    39
  val const_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    40
  val type_const_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    41
  val class_prefix : string
43936
127749bbc639 use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
blanchet
parents: 43907
diff changeset
    42
  val polymorphic_free_prefix : string
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    43
  val skolem_const_prefix : string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    44
  val old_skolem_const_prefix : string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    45
  val new_skolem_const_prefix : string
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    46
  val type_decl_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    47
  val sym_decl_prefix : string
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
    48
  val guards_sym_formula_prefix : string
43129
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
    49
  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
    50
  val fact_prefix : string
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    51
  val conjecture_prefix : string
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    52
  val helper_prefix : string
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    53
  val class_rel_clause_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    54
  val arity_clause_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    55
  val tfree_clause_prefix : string
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    56
  val typed_helper_suffix : string
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    57
  val untyped_helper_suffix : string
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
    58
  val type_tag_idempotence_helper_name : string
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    59
  val predicator_name : string
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    60
  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
    61
  val type_tag_name : string
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    62
  val type_pred_name : string
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
    63
  val simple_type_prefix : string
43174
f497a1e97d37 skip "hBOOL" in new Metis path finder
blanchet
parents: 43167
diff changeset
    64
  val prefixed_predicator_name : string
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
    65
  val prefixed_app_op_name : string
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
    66
  val prefixed_type_tag_name : string
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    67
  val ascii_of : string -> string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    68
  val unascii_of : string -> string
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    69
  val strip_prefix_and_unascii : string -> string -> string option
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
    70
  val proxy_table : (string * (string * (thm * (string * string)))) list
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
    71
  val proxify_const : string -> (string * string) option
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    72
  val invert_const : string -> string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    73
  val unproxify_const : string -> string
43093
blanchet
parents: 43092
diff changeset
    74
  val new_skolem_var_name_from_const : string -> string
43248
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
    75
  val atp_irrelevant_consts : string list
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
    76
  val atp_schematic_consts_of : term -> typ list Symtab.table
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    77
  val is_locality_global : locality -> bool
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    78
  val type_enc_from_string : string -> type_enc
43828
e07a2c4cbad8 move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
blanchet
parents: 43827
diff changeset
    79
  val is_type_enc_higher_order : type_enc -> bool
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    80
  val polymorphism_of_type_enc : type_enc -> polymorphism
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    81
  val level_of_type_enc : type_enc -> type_level
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    82
  val is_type_enc_virtually_sound : type_enc -> bool
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    83
  val is_type_enc_fairly_sound : type_enc -> bool
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    84
  val choose_format : format list -> type_enc -> format * type_enc
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43130
diff changeset
    85
  val mk_aconns :
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43130
diff changeset
    86
    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
    87
  val unmangled_const : string -> string * (string, 'b) ho_term list
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
    88
  val unmangled_const_name : string -> string
43194
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
    89
  val helper_table : ((string * bool) * thm list) list
43501
0e422a84d0b2 don't change the way helpers are generated for the exporter's sake
blanchet
parents: 43496
diff changeset
    90
  val factsN : string
43856
d636b053d4ff move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents: 43830
diff changeset
    91
  val introduce_combinators : Proof.context -> term -> term
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39975
diff changeset
    92
  val prepare_atp_problem :
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    93
    Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
    94
    -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
    95
    -> term -> ((string * locality) * term) list
42541
8938507b2054 move type declarations to the front, for TFF-compliance
blanchet
parents: 42540
diff changeset
    96
    -> string problem * string Symtab.table * int * int
43214
4e850b2c1f5c removed old optimization that isn't one anyone
blanchet
parents: 43213
diff changeset
    97
       * (string * locality) 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
    98
  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
    99
end;
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   100
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   101
structure ATP_Translate : ATP_TRANSLATE =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   102
struct
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   103
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   104
open ATP_Util
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   105
open ATP_Problem
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   106
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   107
type name = string * string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   108
43828
e07a2c4cbad8 move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
blanchet
parents: 43827
diff changeset
   109
val generate_info = false (* experimental *)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   110
43693
b46f5d2d42cc make SML/NJ happier
blanchet
parents: 43692
diff changeset
   111
fun isabelle_info s =
b46f5d2d42cc make SML/NJ happier
blanchet
parents: 43692
diff changeset
   112
  if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
b46f5d2d42cc make SML/NJ happier
blanchet
parents: 43692
diff changeset
   113
  else NONE
42879
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   114
43693
b46f5d2d42cc make SML/NJ happier
blanchet
parents: 43692
diff changeset
   115
val introN = "intro"
b46f5d2d42cc make SML/NJ happier
blanchet
parents: 43692
diff changeset
   116
val elimN = "elim"
b46f5d2d42cc make SML/NJ happier
blanchet
parents: 43692
diff changeset
   117
val simpN = "simp"
42879
3b9669b11d33 generate useful information for type axioms
blanchet
parents: 42878
diff changeset
   118
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   119
val bound_var_prefix = "B_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   120
val schematic_var_prefix = "V_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   121
val fixed_var_prefix = "v_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   122
val tvar_prefix = "T_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   123
val tfree_prefix = "t_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   124
val const_prefix = "c_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   125
val type_const_prefix = "tc_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   126
val class_prefix = "cl_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   127
43936
127749bbc639 use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
blanchet
parents: 43907
diff changeset
   128
val polymorphic_free_prefix = "poly_free"
43907
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   129
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   130
val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   131
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
   132
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
   133
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   134
val type_decl_prefix = "ty_"
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   135
val sym_decl_prefix = "sy_"
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   136
val guards_sym_formula_prefix = "gsy_"
43129
4301f1c123d6 support lightweight tags in new Metis
blanchet
parents: 43128
diff changeset
   137
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
   138
val fact_prefix = "fact_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   139
val conjecture_prefix = "conj_"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   140
val helper_prefix = "help_"
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   141
val class_rel_clause_prefix = "clar_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   142
val arity_clause_prefix = "arity_"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   143
val tfree_clause_prefix = "tfree_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   144
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   145
val lambda_fact_prefix = "ATP.lambda_"
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   146
val typed_helper_suffix = "_T"
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   147
val untyped_helper_suffix = "_U"
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   148
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   149
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   150
val predicator_name = "hBOOL"
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   151
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
   152
val type_tag_name = "ti"
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
   153
val type_pred_name = "is"
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
   154
val simple_type_prefix = "ty_"
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   155
43174
f497a1e97d37 skip "hBOOL" in new Metis path finder
blanchet
parents: 43167
diff changeset
   156
val prefixed_predicator_name = const_prefix ^ predicator_name
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
   157
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
   158
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
   159
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   160
(* Freshness almost guaranteed! *)
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   161
val atp_weak_prefix = "ATP:"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   162
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   163
(*Escaping of special characters.
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   164
  Alphanumeric characters are left unchanged.
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   165
  The character _ goes to __
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   166
  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
   167
  Other characters go to _nnn where nnn is the decimal ASCII code.*)
43093
blanchet
parents: 43092
diff changeset
   168
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
   169
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   170
fun stringN_of_int 0 _ = ""
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   171
  | stringN_of_int k n =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   172
    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
   173
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   174
fun ascii_of_char c =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   175
  if Char.isAlphaNum c then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   176
    String.str c
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   177
  else if c = #"_" then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   178
    "__"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   179
  else if #" " <= c andalso c <= #"/" then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   180
    "_" ^ 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
   181
  else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   182
    (* fixed width, in case more digits follow *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   183
    "_" ^ stringN_of_int 3 (Char.ord c)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   184
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   185
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
   186
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   187
(** 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
   188
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   189
(* 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
   190
   thread. Also, the errors are impossible. *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   191
val unascii_of =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   192
  let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   193
    fun un rcs [] = String.implode(rev rcs)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   194
      | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   195
        (* Three types of _ escapes: __, _A to _P, _nnn *)
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   196
      | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   197
      | un rcs (#"_" :: c :: cs) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   198
        if #"A" <= c andalso c<= #"P" then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   199
          (* translation of #" " to #"/" *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   200
          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
   201
        else
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   202
          let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   203
            case Int.fromString (String.implode digits) of
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   204
              SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   205
            | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   206
          end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   207
      | 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
   208
  in un [] o String.explode end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   209
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   210
(* 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
   211
   un-ASCII'd. *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   212
fun strip_prefix_and_unascii s1 s =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   213
  if String.isPrefix s1 s then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   214
    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
   215
  else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   216
    NONE
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   217
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   218
val proxy_table =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   219
  [("c_False", (@{const_name False}, (@{thm fFalse_def},
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   220
       ("fFalse", @{const_name ATP.fFalse})))),
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   221
   ("c_True", (@{const_name True}, (@{thm fTrue_def},
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   222
       ("fTrue", @{const_name ATP.fTrue})))),
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   223
   ("c_Not", (@{const_name Not}, (@{thm fNot_def},
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   224
       ("fNot", @{const_name ATP.fNot})))),
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   225
   ("c_conj", (@{const_name conj}, (@{thm fconj_def},
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   226
       ("fconj", @{const_name ATP.fconj})))),
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   227
   ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   228
       ("fdisj", @{const_name ATP.fdisj})))),
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   229
   ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   230
       ("fimplies", @{const_name ATP.fimplies})))),
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   231
   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   232
       ("fequal", @{const_name ATP.fequal})))),
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   233
   ("c_All", (@{const_name All}, (@{thm fAll_def},
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   234
       ("fAll", @{const_name ATP.fAll})))),
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   235
   ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   236
       ("fEx", @{const_name ATP.fEx}))))]
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   237
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   238
val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   239
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   240
(* 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
   241
   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
   242
val const_trans_table =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   243
  [(@{type_name Product_Type.prod}, "prod"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   244
   (@{type_name Sum_Type.sum}, "sum"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   245
   (@{const_name False}, "False"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   246
   (@{const_name True}, "True"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   247
   (@{const_name Not}, "Not"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   248
   (@{const_name conj}, "conj"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   249
   (@{const_name disj}, "disj"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   250
   (@{const_name implies}, "implies"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   251
   (@{const_name HOL.eq}, "equal"),
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   252
   (@{const_name All}, "All"),
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   253
   (@{const_name Ex}, "Ex"),
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   254
   (@{const_name If}, "If"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   255
   (@{const_name Set.member}, "member"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   256
   (@{const_name Meson.COMBI}, "COMBI"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   257
   (@{const_name Meson.COMBK}, "COMBK"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   258
   (@{const_name Meson.COMBB}, "COMBB"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   259
   (@{const_name Meson.COMBC}, "COMBC"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   260
   (@{const_name Meson.COMBS}, "COMBS")]
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   261
  |> Symtab.make
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   262
  |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   263
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   264
(* 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
   265
val const_trans_table_inv =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   266
  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
   267
val const_trans_table_unprox =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   268
  Symtab.empty
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   269
  |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   270
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   271
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
   272
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
   273
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   274
fun lookup_const c =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   275
  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
   276
    SOME c' => c'
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   277
  | NONE => ascii_of c
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   278
43622
blanchet
parents: 43572
diff changeset
   279
fun ascii_of_indexname (v, 0) = ascii_of v
blanchet
parents: 43572
diff changeset
   280
  | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   281
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   282
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
   283
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
   284
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
   285
43622
blanchet
parents: 43572
diff changeset
   286
fun make_schematic_type_var (x, i) =
blanchet
parents: 43572
diff changeset
   287
      tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
blanchet
parents: 43572
diff changeset
   288
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   289
43622
blanchet
parents: 43572
diff changeset
   290
(* "HOL.eq" is mapped to the ATP's equality. *)
blanchet
parents: 43572
diff changeset
   291
fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   292
  | 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
   293
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   294
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
   295
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   296
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
   297
43093
blanchet
parents: 43092
diff changeset
   298
fun new_skolem_var_name_from_const s =
blanchet
parents: 43092
diff changeset
   299
  let val ss = s |> space_explode Long_Name.separator in
blanchet
parents: 43092
diff changeset
   300
    nth ss (length ss - 2)
blanchet
parents: 43092
diff changeset
   301
  end
blanchet
parents: 43092
diff changeset
   302
43248
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   303
(* These are either simplified away by "Meson.presimplify" (most of the time) or
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   304
   handled specially via "fFalse", "fTrue", ..., "fequal". *)
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   305
val atp_irrelevant_consts =
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   306
  [@{const_name False}, @{const_name True}, @{const_name Not},
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   307
   @{const_name conj}, @{const_name disj}, @{const_name implies},
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   308
   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   309
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   310
val atp_monomorph_bad_consts =
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   311
  atp_irrelevant_consts @
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   312
  (* These are ignored anyway by the relevance filter (unless they appear in
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   313
     higher-order places) but not by the monomorphizer. *)
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   314
  [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   315
   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   316
   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   317
43258
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   318
fun add_schematic_const (x as (_, T)) =
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   319
  Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   320
val add_schematic_consts_of =
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   321
  Term.fold_aterms (fn Const (x as (s, _)) =>
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   322
                       not (member (op =) atp_monomorph_bad_consts s)
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   323
                       ? add_schematic_const x
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   324
                      | _ => I)
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   325
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
43248
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   326
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   327
(** 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
   328
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   329
(* 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
   330
datatype type_literal =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   331
  TyLitVar of name * name |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   332
  TyLitFree of name * name
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   333
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   334
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   335
(** Isabelle arities **)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   336
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   337
datatype arity_literal =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   338
  TConsLit of name * name * name list |
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   339
  TVarLit of name * name
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   340
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   341
fun gen_TVars 0 = []
43093
blanchet
parents: 43092
diff changeset
   342
  | 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
   343
43263
blanchet
parents: 43259
diff changeset
   344
val type_class = the_single @{sort type}
blanchet
parents: 43259
diff changeset
   345
blanchet
parents: 43259
diff changeset
   346
fun add_packed_sort tvar =
blanchet
parents: 43259
diff changeset
   347
  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   348
43086
blanchet
parents: 43085
diff changeset
   349
type arity_clause =
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   350
  {name : string,
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   351
   prem_lits : arity_literal list,
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   352
   concl_lits : arity_literal}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   353
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   354
(* 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
   355
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
   356
  let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   357
    val tvars = gen_TVars (length args)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   358
    val tvars_srts = ListPair.zip (tvars, args)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   359
  in
43086
blanchet
parents: 43085
diff changeset
   360
    {name = name,
43263
blanchet
parents: 43259
diff changeset
   361
     prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
43086
blanchet
parents: 43085
diff changeset
   362
     concl_lits = TConsLit (`make_type_class cls,
blanchet
parents: 43085
diff changeset
   363
                            `make_fixed_type_const tcons,
blanchet
parents: 43085
diff changeset
   364
                            tvars ~~ tvars)}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   365
  end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   366
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   367
fun arity_clause _ _ (_, []) = []
43495
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   368
  | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   369
    arity_clause seen n (tcons, ars)
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   370
  | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   371
    if member (op =) seen class then
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   372
      (* multiple arities for the same (tycon, class) pair *)
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   373
      make_axiom_arity_clause (tcons,
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   374
          lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   375
          ar) ::
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   376
      arity_clause seen (n + 1) (tcons, ars)
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   377
    else
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   378
      make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   379
                               ascii_of class, ar) ::
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   380
      arity_clause (class :: seen) n (tcons, ars)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   381
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   382
fun multi_arity_clause [] = []
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   383
  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   384
      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
   385
43622
blanchet
parents: 43572
diff changeset
   386
(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
blanchet
parents: 43572
diff changeset
   387
   theory thy provided its arguments have the corresponding sorts. *)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   388
fun type_class_pairs thy tycons classes =
43093
blanchet
parents: 43092
diff changeset
   389
  let
blanchet
parents: 43092
diff changeset
   390
    val alg = Sign.classes_of thy
blanchet
parents: 43092
diff changeset
   391
    fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
blanchet
parents: 43092
diff changeset
   392
    fun add_class tycon class =
blanchet
parents: 43092
diff changeset
   393
      cons (class, domain_sorts tycon class)
blanchet
parents: 43092
diff changeset
   394
      handle Sorts.CLASS_ERROR _ => I
blanchet
parents: 43092
diff changeset
   395
    fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
blanchet
parents: 43092
diff changeset
   396
  in map try_classes tycons end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   397
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   398
(*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
   399
fun iter_type_class_pairs _ _ [] = ([], [])
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   400
  | iter_type_class_pairs thy tycons classes =
43263
blanchet
parents: 43259
diff changeset
   401
      let
blanchet
parents: 43259
diff changeset
   402
        fun maybe_insert_class s =
blanchet
parents: 43259
diff changeset
   403
          (s <> type_class andalso not (member (op =) classes s))
blanchet
parents: 43259
diff changeset
   404
          ? insert (op =) s
blanchet
parents: 43259
diff changeset
   405
        val cpairs = type_class_pairs thy tycons classes
blanchet
parents: 43259
diff changeset
   406
        val newclasses =
blanchet
parents: 43259
diff changeset
   407
          [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
blanchet
parents: 43259
diff changeset
   408
        val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
43266
3baf384e2b99 minor optimization
blanchet
parents: 43265
diff changeset
   409
      in (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
   410
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   411
fun make_arity_clauses thy tycons =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   412
  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
   413
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   414
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   415
(** Isabelle class relations **)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   416
43086
blanchet
parents: 43085
diff changeset
   417
type class_rel_clause =
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   418
  {name : string,
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   419
   subclass : name,
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   420
   superclass : name}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   421
43622
blanchet
parents: 43572
diff changeset
   422
(* Generate all pairs (sub, super) such that sub is a proper subclass of super
blanchet
parents: 43572
diff changeset
   423
   in theory "thy". *)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   424
fun class_pairs _ [] _ = []
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   425
  | class_pairs thy subs supers =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   426
      let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   427
        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
   428
        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
   429
        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
   430
      in fold add_supers subs [] end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   431
43622
blanchet
parents: 43572
diff changeset
   432
fun make_class_rel_clause (sub, super) =
blanchet
parents: 43572
diff changeset
   433
  {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
43086
blanchet
parents: 43085
diff changeset
   434
   superclass = `make_type_class super}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   435
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   436
fun make_class_rel_clauses thy subs supers =
43093
blanchet
parents: 43092
diff changeset
   437
  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
   438
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   439
(* intermediate terms *)
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   440
datatype iterm =
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   441
  IConst of name * typ * typ list |
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   442
  IVar of name * typ |
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   443
  IApp of iterm * iterm |
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   444
  IAbs of (name * typ) * iterm
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   445
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   446
fun ityp_of (IConst (_, T, _)) = T
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   447
  | ityp_of (IVar (_, T)) = T
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   448
  | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   449
  | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
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
(*gets the head of a combinator application, along with the list of arguments*)
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   452
fun strip_iterm_comb u =
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   453
  let
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   454
    fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   455
      | stripc x = x
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   456
  in stripc (u, []) end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   457
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   458
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
   459
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   460
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
   461
  [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
   462
  |> space_implode Long_Name.separator
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   463
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   464
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   465
   Also accumulates sort infomation. *)
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   466
fun iterm_from_term thy bs (P $ Q) =
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   467
    let
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   468
      val (P', P_atomics_Ts) = iterm_from_term thy bs P
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   469
      val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   470
    in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   471
  | iterm_from_term thy _ (Const (c, T)) =
43907
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   472
    (IConst (`make_fixed_const c, T,
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   473
             if String.isPrefix old_skolem_const_prefix c then
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   474
               [] |> Term.add_tvarsT T |> map TVar
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   475
             else
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   476
               (c, T) |> Sign.const_typargs thy),
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   477
     atyps_of T)
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   478
  | iterm_from_term _ _ (Free (s, T)) =
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   479
    (IConst (`make_fixed_var s, T,
43936
127749bbc639 use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
blanchet
parents: 43907
diff changeset
   480
             if String.isPrefix polymorphic_free_prefix s then [T] else []),
43907
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   481
     atyps_of T)
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   482
  | iterm_from_term _ _ (Var (v as (s, _), T)) =
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   483
    (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
   484
       let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   485
         val Ts = T |> strip_type |> swap |> op ::
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   486
         val s' = new_skolem_const_name s (length Ts)
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   487
       in IConst (`make_fixed_const s', T, Ts) end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   488
     else
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   489
       IVar ((make_schematic_var v, s), T), atyps_of T)
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   490
  | iterm_from_term _ bs (Bound j) =
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   491
    nth bs j |> (fn (s, T) => (IConst (`make_bound_var s, T, []), atyps_of T))
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   492
  | iterm_from_term thy bs (Abs (s, T, t)) =
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   493
    let
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   494
      fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   495
      val s = vary s
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   496
      val (tm, atomic_Ts) = iterm_from_term thy ((s, T) :: bs) t
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   497
    in
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   498
      (IAbs ((`make_bound_var s, T), tm),
43677
2cd0b478d1b6 added generation of lambdas in THF
nik
parents: 43676
diff changeset
   499
       union (op =) atomic_Ts (atyps_of T))
2cd0b478d1b6 added generation of lambdas in THF
nik
parents: 43676
diff changeset
   500
    end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   501
43421
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43401
diff changeset
   502
datatype locality =
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43401
diff changeset
   503
  General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43401
diff changeset
   504
  Chained
43085
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
(* (quasi-)underapproximation of the truth *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   507
fun is_locality_global Local = false
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   508
  | is_locality_global Assum = false
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   509
  | is_locality_global Chained = false
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   510
  | is_locality_global _ = true
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   511
43624
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   512
datatype order = First_Order | Higher_Order
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
   513
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
   514
datatype type_level =
43362
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
   515
  All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
   516
  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
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   519
datatype type_enc =
43624
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   520
  Simple_Types of order * type_level |
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   521
  Guards of polymorphism * type_level * type_heaviness |
42837
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
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   527
fun type_enc_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 =>
43624
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   538
          (* "_query" and "_bang" are for the ASCII-challenged Metis and
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   539
             Mirabelle. *)
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   540
          case try_unsuffixes ["?", "_query"] s of
43362
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
   541
            SOME s => (Noninf_Nonmono_Types, 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
   542
          | NONE =>
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   543
            case try_unsuffixes ["!", "_bang"] s of
43362
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
   544
              SOME s => (Fin_Nonmono_Types, 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
   545
            | NONE => (All_Types, s))
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   546
  ||> apsnd (fn s =>
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   547
                case try (unsuffix "_heavy") s of
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   548
                  SOME s => (Heavyweight, s)
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   549
                | NONE => (Lightweight, s))
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   550
  |> (fn (poly, (level, (heaviness, core))) =>
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
   551
         case (core, (poly, level, heaviness)) of
43624
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   552
           ("simple", (NONE, _, Lightweight)) =>
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   553
           Simple_Types (First_Order, level)
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   554
         | ("simple_higher", (NONE, _, Lightweight)) =>
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   555
           if level = Noninf_Nonmono_Types then raise Same.SAME
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   556
           else Simple_Types (Higher_Order, level)
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   557
         | ("guards", (SOME poly, _, _)) => Guards (poly, level, 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
   558
         | ("tags", (SOME Polymorphic, _, _)) =>
43361
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
   559
           Tags (Polymorphic, level, heaviness)
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
   560
         | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   561
         | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   562
           Guards (poly, Const_Arg_Types, Lightweight)
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
   563
         | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   564
           Guards (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
   565
         | _ => 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
   566
  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
   567
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   568
fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   569
  | is_type_enc_higher_order _ = false
43624
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   570
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   571
fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   572
  | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   573
  | polymorphism_of_type_enc (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
   574
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   575
fun level_of_type_enc (Simple_Types (_, level)) = level
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   576
  | level_of_type_enc (Guards (_, level, _)) = level
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   577
  | level_of_type_enc (Tags (_, level, _)) = level
42828
8794ec73ec13 added syntax for "shallow" encodings
blanchet
parents: 42781
diff changeset
   578
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   579
fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   580
  | heaviness_of_type_enc (Guards (_, _, heaviness)) = heaviness
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   581
  | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   582
42687
blanchet
parents: 42685
diff changeset
   583
fun is_type_level_virtually_sound level =
43362
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
   584
  level = All_Types orelse level = Noninf_Nonmono_Types
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   585
val is_type_enc_virtually_sound =
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   586
  is_type_level_virtually_sound o level_of_type_enc
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
   587
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
   588
fun is_type_level_fairly_sound level =
43362
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
   589
  is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   590
val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
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
   591
43624
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   592
fun choose_format formats (Simple_Types (order, level)) =
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   593
    if member (op =) formats THF then
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   594
      (THF, Simple_Types (order, level))
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   595
    else if member (op =) formats TFF then
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   596
      (TFF, Simple_Types (First_Order, level))
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
   597
    else
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   598
      choose_format formats (Guards (Mangled_Monomorphic, level, Heavyweight))
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   599
  | choose_format formats type_enc =
43101
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   600
    (case hd formats of
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   601
       CNF_UEQ =>
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   602
       (CNF_UEQ, case type_enc of
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   603
                   Guards stuff =>
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   604
                   (if is_type_enc_fairly_sound type_enc then Tags else Guards)
43101
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   605
                       stuff
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   606
                 | _ => type_enc)
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   607
     | format => (format, type_enc))
43101
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   608
40114
blanchet
parents: 40069
diff changeset
   609
type translated_formula =
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   610
  {name : string,
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   611
   locality : locality,
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   612
   kind : formula_kind,
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   613
   iformula : (name, typ, iterm) formula,
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   614
   atomic_types : typ list}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   615
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   616
fun update_iformula f ({name, locality, kind, iformula, atomic_types}
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   617
                       : translated_formula) =
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   618
  {name = name, locality = locality, kind = kind, iformula = f iformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   619
   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
   620
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   621
fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
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
   622
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
   623
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
   624
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
   625
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
   626
  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
   627
    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
   628
    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
   629
  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
   630
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
   631
(* 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
   632
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
   633
  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
   634
  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
   635
  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
   636
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   637
fun should_drop_arg_type_args (Simple_Types _) =
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
   638
    false (* since TFF doesn't support overloading *)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   639
  | should_drop_arg_type_args type_enc =
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   640
    level_of_type_enc type_enc = All_Types andalso
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   641
    heaviness_of_type_enc type_enc = Heavyweight
42831
c9b0968484fb more work on "shallow" encoding + adjustments to other encodings
blanchet
parents: 42830
diff changeset
   642
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   643
fun type_arg_policy type_enc s =
43628
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   644
  if s = type_tag_name then
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   645
    (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
43623
e096b1effbbb mangle "ti" tags
blanchet
parents: 43622
diff changeset
   646
       Mangled_Type_Args
e096b1effbbb mangle "ti" tags
blanchet
parents: 43622
diff changeset
   647
     else
e096b1effbbb mangle "ti" tags
blanchet
parents: 43622
diff changeset
   648
       Explicit_Type_Args) false
43628
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   649
  else case type_enc of
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   650
    Tags (_, All_Types, Heavyweight) => No_Type_Args
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   651
  | _ =>
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   652
    if level_of_type_enc type_enc = No_Types orelse
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   653
       s = @{const_name HOL.eq} orelse
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   654
       (s = app_op_name andalso
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   655
        level_of_type_enc type_enc = Const_Arg_Types) then
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   656
      No_Type_Args
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   657
    else
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   658
      should_drop_arg_type_args type_enc
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   659
      |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   660
            Mangled_Type_Args
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   661
          else
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   662
            Explicit_Type_Args)
42227
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 42180
diff changeset
   663
43628
996b2022ff78 further repair "mangled_tags", now that tags are also mangled
blanchet
parents: 43626
diff changeset
   664
(* Make literals for sorted type variables. *)
43263
blanchet
parents: 43259
diff changeset
   665
fun generic_add_sorts_on_type (_, []) = I
blanchet
parents: 43259
diff changeset
   666
  | generic_add_sorts_on_type ((x, i), s :: ss) =
blanchet
parents: 43259
diff changeset
   667
    generic_add_sorts_on_type ((x, i), ss)
blanchet
parents: 43259
diff changeset
   668
    #> (if s = the_single @{sort HOL.type} then
43093
blanchet
parents: 43092
diff changeset
   669
          I
blanchet
parents: 43092
diff changeset
   670
        else if i = ~1 then
43263
blanchet
parents: 43259
diff changeset
   671
          insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
43093
blanchet
parents: 43092
diff changeset
   672
        else
43263
blanchet
parents: 43259
diff changeset
   673
          insert (op =) (TyLitVar (`make_type_class s,
blanchet
parents: 43259
diff changeset
   674
                                   (make_schematic_type_var (x, i), x))))
blanchet
parents: 43259
diff changeset
   675
fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
blanchet
parents: 43259
diff changeset
   676
  | add_sorts_on_tfree _ = I
blanchet
parents: 43259
diff changeset
   677
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
blanchet
parents: 43259
diff changeset
   678
  | add_sorts_on_tvar _ = I
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   679
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   680
fun type_literals_for_types type_enc add_sorts_on_typ Ts =
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   681
  [] |> level_of_type_enc type_enc <> No_Types ? fold add_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
   682
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
   683
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
   684
  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
   685
    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
   686
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   687
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
   688
  | 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
   689
fun mk_aquant _ [] phi = phi
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   690
  | 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
   691
    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
   692
  | 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
   693
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   694
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
   695
  let
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   696
    fun formula_vars bounds (AQuant (_, xs, phi)) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   697
        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
   698
      | 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
   699
      | formula_vars bounds (AAtom tm) =
42526
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   700
        union (op =) (atom_vars tm []
46d485f8d144 added room for types in ATP quantifiers
blanchet
parents: 42525
diff changeset
   701
                      |> 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
   702
  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
   703
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   704
fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2]
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   705
  | iterm_vars (IConst _) = I
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   706
  | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T)
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   707
  | iterm_vars (IAbs (_, tm)) = iterm_vars tm
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   708
fun close_iformula_universally phi = close_universally iterm_vars phi
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   709
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   710
fun term_vars bounds (ATerm (name as (s, _), tms)) =
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   711
    (is_tptp_variable s andalso not (member (op =) bounds name))
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   712
    ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   713
  | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   714
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
   715
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   716
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
   717
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
   718
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   719
fun ho_term_from_typ format type_enc =
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   720
  let
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   721
    fun term (Type (s, Ts)) =
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   722
      ATerm (case (is_type_enc_higher_order type_enc, s) of
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   723
               (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
   724
             | (true, @{type_name fun}) => `I tptp_fun_type
43178
b5862142d378 use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
blanchet
parents: 43175
diff changeset
   725
             | _ => if s = homo_infinite_type_name andalso
b5862142d378 use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
blanchet
parents: 43175
diff changeset
   726
                       (format = TFF orelse format = THF) then
b5862142d378 use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
blanchet
parents: 43175
diff changeset
   727
                      `I tptp_individual_type
b5862142d378 use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
blanchet
parents: 43175
diff changeset
   728
                    else
b5862142d378 use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
blanchet
parents: 43175
diff changeset
   729
                      `make_fixed_type_const s,
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   730
             map term Ts)
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   731
    | 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
   732
    | 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
   733
      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
   734
  in term end
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   735
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   736
fun ho_term_for_type_arg format type_enc T =
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   737
  if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
43401
e93dfcb53535 fixed soundness bug made more visible by previous change
blanchet
parents: 43399
diff changeset
   738
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   739
(* 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
   740
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
   741
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   742
fun generic_mangled_type_name f (ATerm (name, [])) = f name
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   743
  | 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
   744
    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
   745
    ^ ")"
43692
264881a20f50 make SML/NJ happy + tuning
blanchet
parents: 43678
diff changeset
   746
  | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
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
   747
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   748
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
   749
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   750
fun make_simple_type s =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   751
  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
   752
     s = tptp_individual_type then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   753
    s
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   754
  else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   755
    simple_type_prefix ^ ascii_of s
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   756
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   757
fun ho_type_from_ho_term type_enc pred_sym ary =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   758
  let
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   759
    fun to_atype ty =
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   760
      AType ((make_simple_type (generic_mangled_type_name fst ty),
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   761
              generic_mangled_type_name snd ty))
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   762
    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
   763
    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
   764
      | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
43692
264881a20f50 make SML/NJ happy + tuning
blanchet
parents: 43678
diff changeset
   765
      | to_fo _ _ = raise Fail "unexpected type abstraction"
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   766
    fun to_ho (ty as ATerm ((s, _), tys)) =
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   767
        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   768
      | to_ho _ = raise Fail "unexpected type abstraction"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   769
  in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   770
43677
2cd0b478d1b6 added generation of lambdas in THF
nik
parents: 43676
diff changeset
   771
fun ho_type_from_typ format type_enc pred_sym ary =
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   772
  ho_type_from_ho_term type_enc pred_sym ary
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   773
  o ho_term_from_typ format type_enc
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   774
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   775
fun mangled_const_name format type_enc T_args (s, s') =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   776
  let
43676
3b0b448b4d69 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik
parents: 43628
diff changeset
   777
    val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   778
    fun type_suffix f g =
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   779
      fold_rev (curry (op ^) o g o prefix mangled_type_sep
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   780
                o generic_mangled_type_name f) ty_args ""
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   781
  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
   782
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
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
   784
  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
   785
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
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
   787
  (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
   788
   -- 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
   789
                    [] >> 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
   790
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
   791
  (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
   792
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
   793
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
   794
  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
   795
    |> 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
   796
           (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
   797
                                                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
   798
    |> 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
   799
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   800
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
   801
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
   802
  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
   803
    (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
   804
  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
   805
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   806
fun introduce_proxies type_enc =
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   807
  let
43987
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   808
    fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   809
      | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   810
                       _ =
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   811
        (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   812
           limitation. This works in conjuction with special code in
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   813
           "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   814
           possible. *)
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   815
        IAbs ((`I "P", p_T),
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   816
              IApp (IConst (`I ho_quant, T, []),
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   817
                    IAbs ((`I "X", x_T),
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   818
                          IApp (IConst (`I "P", p_T, []),
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   819
                                IConst (`I "X", x_T, [])))))
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   820
      | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   821
    fun intro top_level args (IApp (tm1, tm2)) =
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   822
        IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   823
      | intro top_level args (IConst (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
   824
        (case proxify_const s of
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   825
           SOME proxy_base =>
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   826
           if top_level orelse is_type_enc_higher_order type_enc then
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   827
             case (top_level, s) of
43987
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   828
               (_, "c_False") => IConst (`I tptp_false, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   829
             | (_, "c_True") => IConst (`I tptp_true, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   830
             | (false, "c_Not") => IConst (`I tptp_not, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   831
             | (false, "c_conj") => IConst (`I tptp_and, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   832
             | (false, "c_disj") => IConst (`I tptp_or, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   833
             | (false, "c_implies") => IConst (`I tptp_implies, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   834
             | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   835
             | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
43000
bd424c3dde46 cleaner handling of equality and proxies (esp. for THF)
blanchet
parents: 42998
diff changeset
   836
             | (false, s) =>
43987
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   837
               if is_tptp_equal s then IConst (`I tptp_equal, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   838
               else IConst (proxy_base |>> prefix const_prefix, T, T_args)
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   839
             | _ => IConst (name, T, [])
42569
5737947e4c77 make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents: 42568
diff changeset
   840
           else
43987
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   841
             IConst (proxy_base |>> prefix const_prefix, T, T_args)
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   842
          | NONE => IConst (name, T, T_args))
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   843
      | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   844
      | intro _ _ tm = tm
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   845
  in intro true [] end
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   846
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   847
fun iformula_from_prop thy type_enc eq_as_iff =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   848
  let
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   849
    fun do_term bs t atomic_types =
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   850
      iterm_from_term thy bs (Envir.eta_contract t)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   851
      |>> (introduce_proxies type_enc #> AAtom)
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   852
      ||> union (op =) atomic_types
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   853
    fun do_quant bs q s T t' =
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43304
diff changeset
   854
      let val s = singleton (Name.variant_list (map fst bs)) s in
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   855
        do_formula ((s, T) :: bs) t'
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   856
        #>> mk_aquant q [(`make_bound_var s, SOME T)]
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
   857
      end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   858
    and do_conn bs c t1 t2 =
43198
7a2bc89ac48e whitespace tuning
blanchet
parents: 43194
diff changeset
   859
      do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   860
    and do_formula bs t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   861
      case t of
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   862
        @{const Trueprop} $ t1 => do_formula bs t1
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   863
      | @{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
   864
      | 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
   865
        do_quant bs AForall s T t'
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   866
      | 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
   867
        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
   868
      | @{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
   869
      | @{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
   870
      | @{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
   871
      | 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
   872
        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
   873
      | _ => do_term bs t
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   874
  in do_formula [] end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   875
43264
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 43263
diff changeset
   876
fun presimplify_term _ [] t = t
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 43263
diff changeset
   877
  | presimplify_term ctxt presimp_consts t =
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 43263
diff changeset
   878
    t |> exists_Const (member (op =) presimp_consts o fst) t
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 43263
diff changeset
   879
         ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 43263
diff changeset
   880
            #> Meson.presimplify ctxt
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 43263
diff changeset
   881
            #> prop_of)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   882
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   883
fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   884
fun conceal_bounds Ts t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   885
  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
   886
                    (0 upto length Ts - 1 ~~ Ts), t)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   887
fun reveal_bounds Ts =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   888
  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
   889
                    (0 upto length Ts - 1 ~~ Ts))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   890
43265
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   891
fun is_fun_equality (@{const_name HOL.eq},
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   892
                     Type (_, [Type (@{type_name fun}, _), _])) = true
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   893
  | is_fun_equality _ = false
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   894
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
   895
fun extensionalize_term ctxt t =
43265
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   896
  if exists_Const is_fun_equality t then
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   897
    let val thy = Proof_Context.theory_of ctxt in
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   898
      t |> cterm_of thy |> Meson.extensionalize_conv ctxt
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   899
        |> prop_of |> Logic.dest_equals |> snd
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   900
    end
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   901
  else
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
   902
    t
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
   903
43862
a14fdb8c0497 pass kind to lambda-translation function
blanchet
parents: 43861
diff changeset
   904
fun simple_translate_lambdas do_lambdas ctxt t =
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   905
  let val thy = Proof_Context.theory_of ctxt in
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   906
    if Meson.is_fol_term thy t then
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   907
      t
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   908
    else
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   909
      let
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   910
        fun aux Ts t =
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   911
          case t of
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   912
            @{const Not} $ t1 => @{const Not} $ aux Ts t1
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   913
          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   914
            t0 $ Abs (s, T, aux (T :: Ts) t')
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   915
          | (t0 as Const (@{const_name All}, _)) $ t1 =>
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   916
            aux Ts (t0 $ eta_expand Ts t1 1)
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   917
          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   918
            t0 $ Abs (s, T, aux (T :: Ts) t')
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   919
          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   920
            aux Ts (t0 $ eta_expand Ts t1 1)
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   921
          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   922
          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   923
          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   924
          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   925
              $ t1 $ t2 =>
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   926
            t0 $ aux Ts t1 $ aux Ts t2
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   927
          | _ =>
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   928
            if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   929
            else t |> Envir.eta_contract |> do_lambdas ctxt Ts
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   930
        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   931
      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   932
  end
43856
d636b053d4ff move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents: 43830
diff changeset
   933
43997
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
   934
fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
   935
    do_cheaply_conceal_lambdas Ts t1
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
   936
    $ do_cheaply_conceal_lambdas Ts t2
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
   937
  | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
   938
    Free (polymorphic_free_prefix ^ serial_string (),
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
   939
          T --> fastype_of1 (T :: Ts, t))
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
   940
  | do_cheaply_conceal_lambdas _ t = t
43856
d636b053d4ff move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents: 43830
diff changeset
   941
43862
a14fdb8c0497 pass kind to lambda-translation function
blanchet
parents: 43861
diff changeset
   942
fun do_introduce_combinators ctxt Ts t =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   943
  let val thy = Proof_Context.theory_of ctxt in
43905
1ace987e22e5 avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents: 43864
diff changeset
   944
    t |> conceal_bounds Ts
1ace987e22e5 avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents: 43864
diff changeset
   945
      |> cterm_of thy
1ace987e22e5 avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents: 43864
diff changeset
   946
      |> Meson_Clausify.introduce_combinators_in_cterm
1ace987e22e5 avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents: 43864
diff changeset
   947
      |> prop_of |> Logic.dest_equals |> snd
1ace987e22e5 avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents: 43864
diff changeset
   948
      |> reveal_bounds Ts
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
   949
  end
43862
a14fdb8c0497 pass kind to lambda-translation function
blanchet
parents: 43861
diff changeset
   950
  (* A type variable of sort "{}" will make abstraction fail. *)
43997
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
   951
  handle THM _ => t |> do_cheaply_conceal_lambdas Ts
43862
a14fdb8c0497 pass kind to lambda-translation function
blanchet
parents: 43861
diff changeset
   952
val introduce_combinators = simple_translate_lambdas do_introduce_combinators
a14fdb8c0497 pass kind to lambda-translation function
blanchet
parents: 43861
diff changeset
   953
43864
58a7b3fdc193 fixed lambda-liftg: must ensure the formulas are in close form
blanchet
parents: 43863
diff changeset
   954
fun preprocess_abstractions_in_terms trans_lambdas facts =
43862
a14fdb8c0497 pass kind to lambda-translation function
blanchet
parents: 43861
diff changeset
   955
  let
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   956
    val (facts, lambda_ts) =
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   957
      facts |> map (snd o snd) |> trans_lambdas 
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   958
            |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   959
    val lambda_facts =
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   960
      map2 (fn t => fn j =>
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   961
               ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   962
           lambda_ts (1 upto length lambda_ts)
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   963
  in (facts, lambda_facts) end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   964
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   965
(* 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
   966
   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
   967
fun freeze_term t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   968
  let
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   969
    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
   970
      | 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
   971
      | aux (Var ((s, i), T)) =
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   972
        Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   973
      | aux t = t
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   974
  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
   975
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
   976
fun presimp_prop ctxt presimp_consts t =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   977
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42353
diff changeset
   978
    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
   979
    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
   980
              |> transform_elim_prop
41211
1e2e16bc0077 no need to do a super-duper atomization if Metis fails afterwards anyway
blanchet
parents: 41199
diff changeset
   981
              |> Object_Logic.atomize_term thy
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
   982
    val need_trueprop = (fastype_of t = @{typ bool})
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   983
  in
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   984
    t |> need_trueprop ? HOLogic.mk_Trueprop
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   985
      |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   986
      |> extensionalize_term ctxt
43264
a1a48c69d623 don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents: 43263
diff changeset
   987
      |> presimplify_term ctxt presimp_consts
43120
a9c2cdf4ae97 make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
blanchet
parents: 43105
diff changeset
   988
      |> perhaps (try (HOLogic.dest_Trueprop))
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   989
  end
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   990
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   991
(* making fact and conjecture formulas *)
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   992
fun make_formula thy type_enc eq_as_iff name loc kind t =
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
   993
  let
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   994
    val (iformula, atomic_types) =
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   995
      iformula_from_prop thy type_enc eq_as_iff t []
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   996
  in
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   997
    {name = name, locality = loc, kind = kind, iformula = iformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   998
     atomic_types = atomic_types}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   999
  end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1000
43860
57ef3cd4126e more refactoring of preprocessing, so as to be able to centralize it
blanchet
parents: 43859
diff changeset
  1001
fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
  1002
  let val thy = Proof_Context.theory_of ctxt in
43860
57ef3cd4126e more refactoring of preprocessing, so as to be able to centralize it
blanchet
parents: 43859
diff changeset
  1003
    case t |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
43624
de026aecab9b cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
blanchet
parents: 43623
diff changeset
  1004
                           loc Axiom of
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
  1005
      formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
  1006
      if s = tptp_true then NONE else SOME formula
43295
30aaab778416 pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents: 43293
diff changeset
  1007
    | formula => SOME formula
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
  1008
  end
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
  1009
43860
57ef3cd4126e more refactoring of preprocessing, so as to be able to centralize it
blanchet
parents: 43859
diff changeset
  1010
fun make_conjecture ctxt format type_enc ps =
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
  1011
  let
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
  1012
    val thy = Proof_Context.theory_of ctxt
43860
57ef3cd4126e more refactoring of preprocessing, so as to be able to centralize it
blanchet
parents: 43859
diff changeset
  1013
    val last = length ps - 1
43096
f181d66046d4 don't preprocess twice
blanchet
parents: 43093
diff changeset
  1014
  in
43863
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
  1015
    map2 (fn j => fn ((name, loc), (kind, t)) =>
a43d61270142 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet
parents: 43862
diff changeset
  1016
             t |> make_formula thy type_enc (format <> CNF) name loc kind
43860
57ef3cd4126e more refactoring of preprocessing, so as to be able to centralize it
blanchet
parents: 43859
diff changeset
  1017
               |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
57ef3cd4126e more refactoring of preprocessing, so as to be able to centralize it
blanchet
parents: 43859
diff changeset
  1018
         (0 upto last) ps
38613
4ca2cae2653f use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents: 38610
diff changeset
  1019
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1020
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
  1021
(** 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
  1022
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
  1023
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
  1024
  | 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
  1025
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
  1026
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
  1027
(* 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
  1028
   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
  1029
   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
  1030
   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
  1031
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
  1032
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
  1033
    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
  1034
  | should_encode_type _ _ All_Types _ = true
43572
ae612a423dad added "sound" option to force Sledgehammer to be pedantically sound
blanchet
parents: 43501
diff changeset
  1035
  | should_encode_type ctxt _ Fin_Nonmono_Types T =
ae612a423dad added "sound" option to force Sledgehammer to be pedantically sound
blanchet
parents: 43501
diff changeset
  1036
    is_type_surely_finite ctxt false T
42682
562046fd8e0c added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
blanchet
parents: 42680
diff changeset
  1037
  | 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
  1038
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
  1039
fun should_predicate_on_type ctxt nonmono_Ts (Guards (_, level, heaviness))
42834
40f7691d0539 implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents: 42832
diff changeset
  1040
                             should_predicate_on_var T =
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
  1041
    (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
  1042
    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
  1043
  | 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
  1044
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
  1045
fun is_var_or_bound_var (IConst ((s, _), _, _)) =
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1046
    String.isPrefix bound_var_prefix s
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
  1047
  | is_var_or_bound_var (IVar _) = true
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1048
  | is_var_or_bound_var _ = false
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1049
43361
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1050
datatype tag_site =
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1051
  Top_Level of bool option |
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1052
  Eq_Arg of bool option |
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1053
  Elsewhere
42829
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1054
43361
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1055
fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1056
  | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1057
                         u T =
42837
358769224d94 renamed thin to light, fat to heavy
blanchet
parents: 42836
diff changeset
  1058
    (case heaviness of
43128
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
  1059
       Heavyweight => should_encode_type ctxt nonmono_Ts level T
a19826080596 tuned names
blanchet
parents: 43125
diff changeset
  1060
     | Lightweight =>
42836
9adf6b3965b3 code cleanup, better handling of corner cases
blanchet
parents: 42834
diff changeset
  1061
       case (site, is_var_or_bound_var u) of
43361
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1062
         (Eq_Arg pos, true) =>
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1063
         (* The first disjunct prevents a subtle soundness issue explained in
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1064
            Blanchette's Ph.D. thesis. See also
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1065
            "formula_lines_for_lightweight_tags_sym_decl". *)
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1066
         (pos <> SOME false andalso poly = Polymorphic andalso
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1067
          level <> All_Types andalso heaviness = Lightweight andalso
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1068
          exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
e37b54d429f5 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents: 43324
diff changeset
  1069
         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
  1070
       | _ => false)
1558741f8a72 started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents: 42828
diff changeset
  1071
  | 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
  1072
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1073
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
  1074
  let
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
  1075
    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
  1076
    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
  1077
      | 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
  1078
        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
  1079
      | 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
  1080
  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
  1081
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
  1082
(** "hBOOL" and "hAPP" **)
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
  1083
42574
blanchet
parents: 42573
diff changeset
  1084
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
  1085
  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
42563
e70ffe3846d0 improve helper type instantiation code
blanchet
parents: 42562
diff changeset
  1086
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
  1087
fun add_iterm_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
  1088
  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
  1089
    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
  1090
      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
  1091
        fun iter ary T =
43210
7384b771805d made "explicit_apply"'s smart mode (more) complete
blanchet
parents: 43207
diff changeset
  1092
          if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
7384b771805d made "explicit_apply"'s smart mode (more) complete
blanchet
parents: 43207
diff changeset
  1093
             type_instance ctxt (T, var_T) then
7384b771805d made "explicit_apply"'s smart mode (more) complete
blanchet
parents: 43207
diff changeset
  1094
            ary
7384b771805d made "explicit_apply"'s smart mode (more) complete
blanchet
parents: 43207
diff changeset
  1095
          else
7384b771805d made "explicit_apply"'s smart mode (more) complete
blanchet
parents: 43207
diff changeset
  1096
            iter (ary + 1) (range_type T)
43064
b6e61d22fa61 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents: 43039
diff changeset
  1097
      in iter 0 const_T end
43201
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1098
    fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1099
      if explicit_apply = NONE andalso
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1100
         (can dest_funT T orelse T = @{typ bool}) then
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1101
        let
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1102
          val bool_vars' = bool_vars orelse body_type T = @{typ bool}
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1103
          fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1104
            {pred_sym = pred_sym andalso not bool_vars',
43213
e1fdd27e0c98 generate less type information in polymorphic case
blanchet
parents: 43210
diff changeset
  1105
             min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
43201
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1106
             max_ary = max_ary, types = types}
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1107
          val fun_var_Ts' =
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1108
            fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1109
        in
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1110
          if bool_vars' = bool_vars andalso
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1111
             pointer_eq (fun_var_Ts', fun_var_Ts) then
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1112
            accum
43167
839f599bc7ed ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents: 43159
diff changeset
  1113
          else
43213
e1fdd27e0c98 generate less type information in polymorphic case
blanchet
parents: 43210
diff changeset
  1114
            ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
43201
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1115
        end
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1116
      else
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1117
        accum
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1118
    fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
  1119
      let val (head, args) = strip_iterm_comb tm in
42558
3d9930cb6770 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents: 42557
diff changeset
  1120
        (case head of
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
  1121
           IConst ((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
  1122
           if String.isPrefix bound_var_prefix s then
43201
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1123
             add_var_or_bound_var T 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
  1124
           else
43139
9ed5d8ad8fa0 fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2
blanchet
parents: 43136
diff changeset
  1125
             let val ary = length args in
43201
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1126
               ((bool_vars, fun_var_Ts),
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
  1127
                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
  1128
                  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
  1129
                  let
43201
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1130
                    val pred_sym =
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1131
                      pred_sym andalso top_level andalso not bool_vars
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
  1132
                    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
  1133
                    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
  1134
                      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
  1135
                         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
  1136
                        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
  1137
                      else
43201
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1138
                        fold (consider_var_arity T) fun_var_Ts min_ary
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
  1139
                  in
43201
0c9bf1a8e0d8 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
blanchet
parents: 43198
diff changeset
  1140
                    Symtab.update (s, {pred_sym = pred_sym,
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
  1141
                                       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
  1142
                                       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
  1143
                                       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
  1144
                                  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
  1145
                  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
  1146
                | 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