src/HOL/Tools/ATP/atp_problem_generate.ML
author blanchet
Tue, 31 Jan 2012 10:29:04 +0100
changeset 46377 dce6c3a460a9
parent 46375 d724066ff3d0
child 46379 de5dd84717c1
permissions -rw-r--r--
new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
     1
(*  Title:      HOL/Tools/ATP/atp_problem_generate.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
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
     9
signature ATP_PROBLEM_GENERATE =
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
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 45299
diff changeset
    14
  type atp_format = ATP_Problem.atp_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
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46339
diff changeset
    18
  datatype scope = Global | Local | Assum | Chained
46341
ab9d96cc7a99 even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
blanchet
parents: 46340
diff changeset
    19
  datatype status = General | Induct | Intro | Elim | Simp | Eq
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46339
diff changeset
    20
  type stature = scope * status
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
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44493
diff changeset
    22
  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46093
diff changeset
    23
  datatype strictness = Strict | Non_Strict
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
    24
  datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
    25
  datatype type_level =
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44396
diff changeset
    26
    All_Types |
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46093
diff changeset
    27
    Noninf_Nonmono_Types of strictness * granularity |
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
    28
    Fin_Nonmono_Types of granularity |
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44396
diff changeset
    29
    Const_Arg_Types |
43362
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
    30
    No_Types
44782
blanchet
parents: 44774
diff changeset
    31
  type 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
    32
44496
c1884789ff80 added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents: 44495
diff changeset
    33
  val type_tag_idempotence : bool Config.T
c1884789ff80 added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents: 44495
diff changeset
    34
  val type_tag_arguments : bool Config.T
45513
25388cf06437 rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents: 45511
diff changeset
    35
  val no_lamsN : string
25388cf06437 rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents: 45511
diff changeset
    36
  val hide_lamsN : string
46365
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46341
diff changeset
    37
  val liftingN : string
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46341
diff changeset
    38
  val combsN : string
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46341
diff changeset
    39
  val combs_and_liftingN : string
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46341
diff changeset
    40
  val combs_or_liftingN : string
45513
25388cf06437 rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents: 45511
diff changeset
    41
  val lam_liftingN : string
25388cf06437 rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents: 45511
diff changeset
    42
  val keep_lamsN : string
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    43
  val schematic_var_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    44
  val fixed_var_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    45
  val tvar_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    46
  val tfree_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    47
  val const_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    48
  val type_const_prefix : string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    49
  val class_prefix : string
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
    50
  val lam_lifted_prefix : string
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
    51
  val lam_lifted_mono_prefix : string
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
    52
  val lam_lifted_poly_prefix : string
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    53
  val skolem_const_prefix : string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    54
  val old_skolem_const_prefix : string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    55
  val new_skolem_const_prefix : string
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
    56
  val combinator_prefix : string
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    57
  val type_decl_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    58
  val sym_decl_prefix : string
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
    59
  val guards_sym_formula_prefix : string
44396
66b9b3fcd608 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
blanchet
parents: 44394
diff changeset
    60
  val 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
    61
  val fact_prefix : string
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
    62
  val conjecture_prefix : string
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    63
  val helper_prefix : string
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    64
  val class_rel_clause_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    65
  val arity_clause_prefix : string
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    66
  val tfree_clause_prefix : string
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
    67
  val lam_fact_prefix : string
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
    68
  val typed_helper_suffix : string
43125
ddf63baabdec distinguish different kinds of typing informations in the fact name
blanchet
parents: 43121
diff changeset
    69
  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
    70
  val type_tag_idempotence_helper_name : string
42966
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    71
  val predicator_name : string
4e2d6c1e5392 more work on parsing LEO-II proofs without lambdas
blanchet
parents: 42963
diff changeset
    72
  val app_op_name : string
44396
66b9b3fcd608 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
blanchet
parents: 44394
diff changeset
    73
  val type_guard_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
    74
  val type_tag_name : string
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42956
diff changeset
    75
  val simple_type_prefix : string
43174
f497a1e97d37 skip "hBOOL" in new Metis path finder
blanchet
parents: 43167
diff changeset
    76
  val prefixed_predicator_name : string
43130
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
    77
  val prefixed_app_op_name : string
d73fc2e55308 implemented missing hAPP and ti cases of new path finder
blanchet
parents: 43129
diff changeset
    78
  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
    79
  val ascii_of : string -> string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    80
  val unascii_of : string -> string
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45509
diff changeset
    81
  val unprefix_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
    82
  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
    83
  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
    84
  val invert_const : string -> string
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
    85
  val unproxify_const : string -> string
43093
blanchet
parents: 43092
diff changeset
    86
  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
    87
  val atp_irrelevant_consts : string list
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
    88
  val atp_schematic_consts_of : term -> typ list Symtab.table
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
    89
  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
    90
  val polymorphism_of_type_enc : type_enc -> polymorphism
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    91
  val level_of_type_enc : type_enc -> type_level
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44396
diff changeset
    92
  val is_type_enc_quasi_sound : type_enc -> bool
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
    93
  val is_type_enc_fairly_sound : type_enc -> bool
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46093
diff changeset
    94
  val type_enc_from_string : strictness -> string -> type_enc
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 45299
diff changeset
    95
  val adjust_type_enc : atp_format -> type_enc -> type_enc
43136
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43130
diff changeset
    96
  val mk_aconns :
cf5cda219058 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents: 43130
diff changeset
    97
    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
    98
  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
    99
  val unmangled_const_name : string -> string
43194
ef3ff8856245 fixed type helper indices in new Metis
blanchet
parents: 43193
diff changeset
   100
  val helper_table : ((string * bool) * thm list) list
45514
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45513
diff changeset
   101
  val trans_lams_from_string :
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45513
diff changeset
   102
    Proof.context -> type_enc -> string -> term list -> term list * term list
43501
0e422a84d0b2 don't change the way helpers are generated for the exporter's sake
blanchet
parents: 43496
diff changeset
   103
  val factsN : string
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39975
diff changeset
   104
  val prepare_atp_problem :
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 45299
diff changeset
   105
    Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44396
diff changeset
   106
    -> bool -> string -> bool -> bool -> term list -> term
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46339
diff changeset
   107
    -> ((string * stature) * term) list
cac402c486b0 separate orthogonal components
blanchet
parents: 46339
diff changeset
   108
    -> string problem * string Symtab.table * (string * stature) list vector
45551
a62c7a21f4ab removed needless baggage
blanchet
parents: 45520
diff changeset
   109
       * (string * term) list * int Symtab.table
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41211
diff changeset
   110
  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
   111
end;
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   112
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
   113
structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   114
struct
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   115
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   116
open ATP_Util
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   117
open ATP_Problem
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   118
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   119
type name = string * string
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   120
44496
c1884789ff80 added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents: 44495
diff changeset
   121
val type_tag_idempotence =
44540
968115499161 change default for generation of tag idempotence and tag argument equations
blanchet
parents: 44508
diff changeset
   122
  Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
44496
c1884789ff80 added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents: 44495
diff changeset
   123
val type_tag_arguments =
44540
968115499161 change default for generation of tag idempotence and tag argument equations
blanchet
parents: 44508
diff changeset
   124
  Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
44496
c1884789ff80 added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents: 44495
diff changeset
   125
45516
b2c8422833da document "lam_trans" option
blanchet
parents: 45514
diff changeset
   126
val no_lamsN = "no_lams" (* used internally; undocumented *)
45513
25388cf06437 rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents: 45511
diff changeset
   127
val hide_lamsN = "hide_lams"
46365
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46341
diff changeset
   128
val liftingN = "lifting"
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46341
diff changeset
   129
val combsN = "combs"
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46341
diff changeset
   130
val combs_and_liftingN = "combs_and_lifting"
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46341
diff changeset
   131
val combs_or_liftingN = "combs_or_lifting"
45513
25388cf06437 rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents: 45511
diff changeset
   132
val keep_lamsN = "keep_lams"
46365
547d1a1dcaf6 rename lambda translation schemes
blanchet
parents: 46341
diff changeset
   133
val lam_liftingN = "lam_lifting" (* legacy *)
44088
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   134
45779
eb7b74c7a69b updated TFF1 support
blanchet
parents: 45570
diff changeset
   135
(* It's still unclear whether all TFF1 implementations will support type
eb7b74c7a69b updated TFF1 support
blanchet
parents: 45570
diff changeset
   136
   signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
eb7b74c7a69b updated TFF1 support
blanchet
parents: 45570
diff changeset
   137
val avoid_first_order_ghost_type_vars = false
44622
779f79ed0ddc avoid relying on dubious TFF1 feature
blanchet
parents: 44595
diff changeset
   138
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   139
val bound_var_prefix = "B_"
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
   140
val all_bound_var_prefix = "BA_"
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
   141
val exist_bound_var_prefix = "BE_"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   142
val schematic_var_prefix = "V_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   143
val fixed_var_prefix = "v_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   144
val tvar_prefix = "T_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   145
val tfree_prefix = "t_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   146
val const_prefix = "c_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   147
val type_const_prefix = "tc_"
44491
ba22ed224b20 fixed bang encoding detection of which types to encode
blanchet
parents: 44463
diff changeset
   148
val simple_type_prefix = "s_"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   149
val class_prefix = "cl_"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   150
45509
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   151
(* Freshness almost guaranteed! *)
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   152
val atp_weak_prefix = "ATP:"
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   153
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   154
val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   155
val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   156
val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
43907
073ab5379842 pass type arguments to lambda-lifted Frees, to account for polymorphism
blanchet
parents: 43906
diff changeset
   157
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
   158
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
   159
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
   160
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
   161
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   162
val combinator_prefix = "COMB"
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   163
42998
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   164
val type_decl_prefix = "ty_"
1c80902d0456 fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents: 42994
diff changeset
   165
val sym_decl_prefix = "sy_"
43989
eb763b3ff9ed renamed "preds" encodings to "guards"
blanchet
parents: 43987
diff changeset
   166
val guards_sym_formula_prefix = "gsy_"
44396
66b9b3fcd608 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
blanchet
parents: 44394
diff changeset
   167
val 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
   168
val fact_prefix = "fact_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   169
val conjecture_prefix = "conj_"
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   170
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
   171
val class_rel_clause_prefix = "clar_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   172
val arity_clause_prefix = "arity_"
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   173
val tfree_clause_prefix = "tfree_"
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   174
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   175
val lam_fact_prefix = "ATP.lambda_"
42881
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   176
val typed_helper_suffix = "_T"
dbdfe2d5b6ab automatically use "metisFT" when typed helpers are necessary
blanchet
parents: 42879
diff changeset
   177
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
   178
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
   179
44491
ba22ed224b20 fixed bang encoding detection of which types to encode
blanchet
parents: 44463
diff changeset
   180
val predicator_name = "pp"
ba22ed224b20 fixed bang encoding detection of which types to encode
blanchet
parents: 44463
diff changeset
   181
val app_op_name = "aa"
ba22ed224b20 fixed bang encoding detection of which types to encode
blanchet
parents: 44463
diff changeset
   182
val type_guard_name = "gg"
ba22ed224b20 fixed bang encoding detection of which types to encode
blanchet
parents: 44463
diff changeset
   183
val type_tag_name = "tt"
42531
a462dbaa584f added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents: 42530
diff changeset
   184
43174
f497a1e97d37 skip "hBOOL" in new Metis path finder
blanchet
parents: 43167
diff changeset
   185
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
   186
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
   187
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
   188
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   189
(*Escaping of special characters.
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   190
  Alphanumeric characters are left unchanged.
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   191
  The character _ goes to __
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   192
  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
   193
  Other characters go to _nnn where nnn is the decimal ASCII code.*)
43093
blanchet
parents: 43092
diff changeset
   194
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
   195
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   196
fun stringN_of_int 0 _ = ""
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   197
  | stringN_of_int k n =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   198
    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
   199
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   200
fun ascii_of_char c =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   201
  if Char.isAlphaNum c then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   202
    String.str c
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   203
  else if c = #"_" then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   204
    "__"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   205
  else if #" " <= c andalso c <= #"/" then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   206
    "_" ^ 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
   207
  else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   208
    (* fixed width, in case more digits follow *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   209
    "_" ^ stringN_of_int 3 (Char.ord c)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   210
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   211
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
   212
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   213
(** 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
   214
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   215
(* 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
   216
   thread. Also, the errors are impossible. *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   217
val unascii_of =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   218
  let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   219
    fun un rcs [] = String.implode(rev rcs)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   220
      | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   221
        (* 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
   222
      | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   223
      | un rcs (#"_" :: c :: cs) =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   224
        if #"A" <= c andalso c<= #"P" then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   225
          (* translation of #" " to #"/" *)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   226
          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
   227
        else
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   228
          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
   229
            case Int.fromString (String.implode digits) of
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   230
              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
   231
            | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   232
          end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   233
      | 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
   234
  in un [] o String.explode end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   235
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   236
(* 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
   237
   un-ASCII'd. *)
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45509
diff changeset
   238
fun unprefix_and_unascii s1 s =
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   239
  if String.isPrefix s1 s then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   240
    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
   241
  else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   242
    NONE
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   243
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   244
val proxy_table =
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   245
  [("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
   246
       ("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
   247
   ("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
   248
       ("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
   249
   ("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
   250
       ("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
   251
   ("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
   252
       ("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
   253
   ("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
   254
       ("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
   255
   ("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
   256
       ("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
   257
   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   258
       ("fequal", @{const_name ATP.fequal})))),
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   259
   ("c_All", (@{const_name All}, (@{thm fAll_def},
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   260
       ("fAll", @{const_name ATP.fAll})))),
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   261
   ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   262
       ("fEx", @{const_name ATP.fEx}))))]
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   263
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   264
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
   265
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   266
(* 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
   267
   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
   268
val const_trans_table =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   269
  [(@{type_name Product_Type.prod}, "prod"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   270
   (@{type_name Sum_Type.sum}, "sum"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   271
   (@{const_name False}, "False"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   272
   (@{const_name True}, "True"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   273
   (@{const_name Not}, "Not"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   274
   (@{const_name conj}, "conj"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   275
   (@{const_name disj}, "disj"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   276
   (@{const_name implies}, "implies"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   277
   (@{const_name HOL.eq}, "equal"),
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   278
   (@{const_name All}, "All"),
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   279
   (@{const_name Ex}, "Ex"),
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   280
   (@{const_name If}, "If"),
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   281
   (@{const_name Set.member}, "member"),
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   282
   (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   283
   (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   284
   (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   285
   (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   286
   (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   287
  |> Symtab.make
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   288
  |> 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
   289
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   290
(* 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
   291
val const_trans_table_inv =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   292
  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
   293
val const_trans_table_unprox =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   294
  Symtab.empty
43159
29b55f292e0b added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents: 43139
diff changeset
   295
  |> 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
   296
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   297
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
   298
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
   299
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   300
fun lookup_const c =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   301
  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
   302
    SOME c' => c'
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   303
  | NONE => ascii_of c
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   304
43622
blanchet
parents: 43572
diff changeset
   305
fun ascii_of_indexname (v, 0) = ascii_of v
blanchet
parents: 43572
diff changeset
   306
  | 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
   307
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   308
fun make_bound_var x = bound_var_prefix ^ ascii_of x
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
   309
fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
   310
fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   311
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
   312
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
   313
43622
blanchet
parents: 43572
diff changeset
   314
fun make_schematic_type_var (x, i) =
44595
444d111bde7d generate properly typed TFF1 (PFF) problems in the presence of type class predicates
blanchet
parents: 44594
diff changeset
   315
  tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
43622
blanchet
parents: 43572
diff changeset
   316
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
   317
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 45299
diff changeset
   318
(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
44587
0f50f158eb57 removed explicit reliance on Hilbert_Choice.Eps
nik
parents: 44586
diff changeset
   319
local
0f50f158eb57 removed explicit reliance on Hilbert_Choice.Eps
nik
parents: 44586
diff changeset
   320
  val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
0f50f158eb57 removed explicit reliance on Hilbert_Choice.Eps
nik
parents: 44586
diff changeset
   321
  fun default c = const_prefix ^ lookup_const c
0f50f158eb57 removed explicit reliance on Hilbert_Choice.Eps
nik
parents: 44586
diff changeset
   322
in
0f50f158eb57 removed explicit reliance on Hilbert_Choice.Eps
nik
parents: 44586
diff changeset
   323
  fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   324
    | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   325
      if c = choice_const then tptp_choice else default c
44587
0f50f158eb57 removed explicit reliance on Hilbert_Choice.Eps
nik
parents: 44586
diff changeset
   326
    | make_fixed_const _ c = default c
0f50f158eb57 removed explicit reliance on Hilbert_Choice.Eps
nik
parents: 44586
diff changeset
   327
end
43085
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
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
   330
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   331
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
   332
43093
blanchet
parents: 43092
diff changeset
   333
fun new_skolem_var_name_from_const s =
blanchet
parents: 43092
diff changeset
   334
  let val ss = s |> space_explode Long_Name.separator in
blanchet
parents: 43092
diff changeset
   335
    nth ss (length ss - 2)
blanchet
parents: 43092
diff changeset
   336
  end
blanchet
parents: 43092
diff changeset
   337
43248
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   338
(* 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
   339
   handled specially via "fFalse", "fTrue", ..., "fequal". *)
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   340
val atp_irrelevant_consts =
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   341
  [@{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
   342
   @{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
   343
   @{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
   344
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   345
val atp_monomorph_bad_consts =
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   346
  atp_irrelevant_consts @
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   347
  (* 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
   348
     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
   349
  [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
69375eaa9016 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents: 43222
diff changeset
   350
   @{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
   351
   @{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
   352
43258
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   353
fun add_schematic_const (x as (_, T)) =
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   354
  Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   355
val add_schematic_consts_of =
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   356
  Term.fold_aterms (fn Const (x as (s, _)) =>
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   357
                       not (member (op =) atp_monomorph_bad_consts s)
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   358
                       ? add_schematic_const x
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   359
                      | _ => I)
956895f99904 slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents: 43248
diff changeset
   360
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
   361
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   362
(** 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
   363
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   364
(** Isabelle arities **)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   365
44625
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   366
type arity_atom = name * name * name list
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   367
43263
blanchet
parents: 43259
diff changeset
   368
val type_class = the_single @{sort type}
blanchet
parents: 43259
diff changeset
   369
43086
blanchet
parents: 43085
diff changeset
   370
type arity_clause =
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   371
  {name : string,
44625
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   372
   prem_atoms : arity_atom list,
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   373
   concl_atom : arity_atom}
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   374
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   375
fun add_prem_atom tvar =
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   376
  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
   377
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   378
(* 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
   379
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
   380
  let
44595
444d111bde7d generate properly typed TFF1 (PFF) problems in the presence of type class predicates
blanchet
parents: 44594
diff changeset
   381
    val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   382
    val tvars_srts = ListPair.zip (tvars, args)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   383
  in
43086
blanchet
parents: 43085
diff changeset
   384
    {name = name,
44625
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   385
     prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   386
     concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   387
                   tvars ~~ tvars)}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   388
  end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   389
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   390
fun arity_clause _ _ (_, []) = []
43495
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   391
  | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   392
    arity_clause seen n (tcons, ars)
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   393
  | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   394
    if member (op =) seen class then
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   395
      (* multiple arities for the same (tycon, class) pair *)
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   396
      make_axiom_arity_clause (tcons,
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   397
          lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   398
          ar) ::
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   399
      arity_clause seen (n + 1) (tcons, ars)
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   400
    else
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   401
      make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   402
                               ascii_of class, ar) ::
75d2e48c5d30 avoid double ASCII-fication
blanchet
parents: 43493
diff changeset
   403
      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
   404
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   405
fun multi_arity_clause [] = []
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   406
  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
44772
blanchet
parents: 44771
diff changeset
   407
    arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   408
43622
blanchet
parents: 43572
diff changeset
   409
(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
blanchet
parents: 43572
diff changeset
   410
   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
   411
fun type_class_pairs thy tycons classes =
43093
blanchet
parents: 43092
diff changeset
   412
  let
blanchet
parents: 43092
diff changeset
   413
    val alg = Sign.classes_of thy
blanchet
parents: 43092
diff changeset
   414
    fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
blanchet
parents: 43092
diff changeset
   415
    fun add_class tycon class =
blanchet
parents: 43092
diff changeset
   416
      cons (class, domain_sorts tycon class)
blanchet
parents: 43092
diff changeset
   417
      handle Sorts.CLASS_ERROR _ => I
blanchet
parents: 43092
diff changeset
   418
    fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
blanchet
parents: 43092
diff changeset
   419
  in map try_classes tycons end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   420
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   421
(*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
   422
fun iter_type_class_pairs _ _ [] = ([], [])
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   423
  | iter_type_class_pairs thy tycons classes =
43263
blanchet
parents: 43259
diff changeset
   424
      let
blanchet
parents: 43259
diff changeset
   425
        fun maybe_insert_class s =
blanchet
parents: 43259
diff changeset
   426
          (s <> type_class andalso not (member (op =) classes s))
blanchet
parents: 43259
diff changeset
   427
          ? insert (op =) s
blanchet
parents: 43259
diff changeset
   428
        val cpairs = type_class_pairs thy tycons classes
blanchet
parents: 43259
diff changeset
   429
        val newclasses =
blanchet
parents: 43259
diff changeset
   430
          [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
blanchet
parents: 43259
diff changeset
   431
        val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
43266
3baf384e2b99 minor optimization
blanchet
parents: 43265
diff changeset
   432
      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
   433
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   434
fun make_arity_clauses thy tycons =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   435
  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
   436
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   437
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   438
(** Isabelle class relations **)
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   439
43086
blanchet
parents: 43085
diff changeset
   440
type class_rel_clause =
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   441
  {name : string,
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   442
   subclass : name,
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   443
   superclass : name}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   444
43622
blanchet
parents: 43572
diff changeset
   445
(* Generate all pairs (sub, super) such that sub is a proper subclass of super
blanchet
parents: 43572
diff changeset
   446
   in theory "thy". *)
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   447
fun class_pairs _ [] _ = []
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   448
  | class_pairs thy subs supers =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   449
      let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   450
        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
   451
        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
   452
        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
   453
      in fold add_supers subs [] end
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   454
43622
blanchet
parents: 43572
diff changeset
   455
fun make_class_rel_clause (sub, super) =
blanchet
parents: 43572
diff changeset
   456
  {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
43086
blanchet
parents: 43085
diff changeset
   457
   superclass = `make_type_class super}
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   458
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   459
fun make_class_rel_clauses thy subs supers =
43093
blanchet
parents: 43092
diff changeset
   460
  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
   461
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   462
(* intermediate terms *)
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   463
datatype iterm =
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   464
  IConst of name * typ * typ list |
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   465
  IVar of name * typ |
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   466
  IApp of iterm * iterm |
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   467
  IAbs of (name * typ) * iterm
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   468
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   469
fun ityp_of (IConst (_, T, _)) = T
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   470
  | ityp_of (IVar (_, T)) = T
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   471
  | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   472
  | 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
   473
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   474
(*gets the head of a combinator application, along with the list of arguments*)
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   475
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
   476
  let
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   477
    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
   478
      | stripc x = x
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   479
  in stripc (u, []) end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   480
45316
08d84bdd5b37 improve handling of bound type variables (esp. for TFF1)
blanchet
parents: 45315
diff changeset
   481
fun atomic_types_of T = fold_atyps (insert (op =)) T []
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   482
45509
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   483
val tvar_a_str = "'a"
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   484
val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   485
val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   486
val itself_name = `make_fixed_type_const @{type_name itself}
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   487
val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   488
val tvar_a_atype = AType (tvar_a_name, [])
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   489
val a_itself_atype = AType (itself_name, [tvar_a_atype])
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   490
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   491
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
   492
  [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
   493
  |> space_implode Long_Name.separator
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   494
44594
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   495
fun robust_const_type thy s =
45509
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   496
  if s = app_op_name then
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   497
    Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   498
  else if String.isPrefix lam_lifted_prefix s then
45509
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   499
    Logic.varifyT_global @{typ "'a => 'b"}
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   500
  else
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   501
    (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   502
    s |> Sign.the_const_type thy
44594
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   503
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   504
(* This function only makes sense if "T" is as general as possible. *)
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   505
fun robust_const_typargs thy (s, T) =
45509
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   506
  if s = app_op_name then
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   507
    let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   508
  else if String.isPrefix old_skolem_const_prefix s then
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   509
    [] |> Term.add_tvarsT T |> rev |> map TVar
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   510
  else if String.isPrefix lam_lifted_prefix s then
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   511
    if String.isPrefix lam_lifted_poly_prefix s then
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45509
diff changeset
   512
      let val (T1, T2) = T |> dest_funT in [T1, T2] end
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45509
diff changeset
   513
    else
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45509
diff changeset
   514
      []
45509
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   515
  else
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   516
    (s, T) |> Sign.const_typargs thy
44594
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   517
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   518
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   519
   Also accumulates sort infomation. *)
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   520
fun iterm_from_term thy format bs (P $ Q) =
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   521
    let
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   522
      val (P', P_atomics_Ts) = iterm_from_term thy format bs P
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   523
      val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   524
    in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   525
  | iterm_from_term thy format _ (Const (c, T)) =
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   526
    (IConst (`(make_fixed_const (SOME format)) c, T,
44594
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   527
             robust_const_typargs thy (c, T)),
45316
08d84bdd5b37 improve handling of bound type variables (esp. for TFF1)
blanchet
parents: 45315
diff changeset
   528
     atomic_types_of T)
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   529
  | iterm_from_term _ _ _ (Free (s, T)) =
45509
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   530
    (IConst (`make_fixed_var s, T, []), atomic_types_of T)
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   531
  | iterm_from_term _ format _ (Var (v as (s, _), T)) =
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   532
    (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
   533
       let
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   534
         val Ts = T |> strip_type |> swap |> op ::
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   535
         val s' = new_skolem_const_name s (length Ts)
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   536
       in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   537
     else
45316
08d84bdd5b37 improve handling of bound type variables (esp. for TFF1)
blanchet
parents: 45315
diff changeset
   538
       IVar ((make_schematic_var v, s), T), atomic_types_of T)
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   539
  | iterm_from_term _ _ bs (Bound j) =
45316
08d84bdd5b37 improve handling of bound type variables (esp. for TFF1)
blanchet
parents: 45315
diff changeset
   540
    nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   541
  | iterm_from_term thy format bs (Abs (s, T, t)) =
43678
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   542
    let
56d352659500 improved translation of lambdas in THF
nik
parents: 43677
diff changeset
   543
      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
   544
      val s = vary s
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
   545
      val name = `make_bound_var s
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
   546
      val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
45316
08d84bdd5b37 improve handling of bound type variables (esp. for TFF1)
blanchet
parents: 45315
diff changeset
   547
    in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   548
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46339
diff changeset
   549
datatype scope = Global | Local | Assum | Chained
46341
ab9d96cc7a99 even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
blanchet
parents: 46340
diff changeset
   550
datatype status = General | Induct | Intro | Elim | Simp | Eq
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46339
diff changeset
   551
type stature = scope * status
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   552
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
   553
datatype order = First_Order | Higher_Order
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44493
diff changeset
   554
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46093
diff changeset
   555
datatype strictness = Strict | Non_Strict
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   556
datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
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
   557
datatype type_level =
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44396
diff changeset
   558
  All_Types |
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46093
diff changeset
   559
  Noninf_Nonmono_Types of strictness * granularity |
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   560
  Fin_Nonmono_Types of granularity |
44397
06375952f1fa cleaner handling of polymorphic monotonicity inference
blanchet
parents: 44396
diff changeset
   561
  Const_Arg_Types |
43362
8d3a5b7b9a00 name tuning
blanchet
parents: 43361
diff changeset
   562
  No_Types
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42612
diff changeset
   563
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   564
datatype type_enc =
44591
0b107d11f634 extended simple types with polymorphism -- the implementation still needs some work though
blanchet
parents: 44589
diff changeset
   565
  Simple_Types of order * polymorphism * type_level |
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   566
  Guards of polymorphism * type_level |
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   567
  Tags of polymorphism * type_level
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   568
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   569
fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   570
  | is_type_enc_higher_order _ = false
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   571
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   572
fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   573
  | polymorphism_of_type_enc (Guards (poly, _)) = poly
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   574
  | polymorphism_of_type_enc (Tags (poly, _)) = poly
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   575
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   576
fun level_of_type_enc (Simple_Types (_, _, level)) = level
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   577
  | level_of_type_enc (Guards (_, level)) = level
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   578
  | level_of_type_enc (Tags (_, level)) = level
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   579
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   580
fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   581
  | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   582
  | granularity_of_type_level _ = All_Vars
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   583
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   584
fun is_type_level_quasi_sound All_Types = true
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   585
  | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   586
  | is_type_level_quasi_sound _ = false
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   587
val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   588
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   589
fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   590
  | is_type_level_fairly_sound level = is_type_level_quasi_sound level
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   591
val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   592
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   593
fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   594
  | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   595
  | is_type_level_monotonicity_based _ = false
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
   596
44785
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   597
(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   598
   Mirabelle. *)
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   599
val queries = ["?", "_query"]
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   600
val bangs = ["!", "_bang"]
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   601
val ats = ["@", "_at"]
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   602
42689
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   603
fun try_unsuffixes ss s =
e38590764c34 versions of ! and ? for the ASCII-challenged Mirabelle
blanchet
parents: 42688
diff changeset
   604
  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
   605
44785
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   606
fun try_nonmono constr suffixes fallback s =
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   607
  case try_unsuffixes suffixes s of
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   608
    SOME s =>
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   609
    (case try_unsuffixes suffixes s of
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   610
       SOME s => (constr Positively_Naked_Vars, s)
44785
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   611
     | NONE =>
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   612
       case try_unsuffixes ats s of
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   613
         SOME s => (constr Ghost_Type_Arg_Vars, s)
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   614
       | NONE => (constr All_Vars, s))
44785
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   615
  | NONE => fallback s
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   616
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46093
diff changeset
   617
fun type_enc_from_string strictness s =
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   618
  (case try (unprefix "poly_") s of
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   619
     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
   620
   | NONE =>
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44493
diff changeset
   621
     case try (unprefix "raw_mono_") s of
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44493
diff changeset
   622
       SOME s => (SOME Raw_Monomorphic, s)
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   623
     | NONE =>
44494
a77901b3774e rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents: 44493
diff changeset
   624
       case try (unprefix "mono_") s of
42722
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   625
         SOME s => (SOME Mangled_Monomorphic, s)
626e292d22a7 renamed type systems for more consistency
blanchet
parents: 42709
diff changeset
   626
       | NONE => (NONE, s))
44785
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   627
  ||> (pair All_Types
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   628
       |> try_nonmono Fin_Nonmono_Types bangs
46301
e2e52c7d25c9 renamed "sound" option to "strict"
blanchet
parents: 46093
diff changeset
   629
       |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   630
  |> (fn (poly, (level, core)) =>
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   631
         case (core, (poly, level)) of
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   632
           ("simple", (SOME poly, _)) =>
44742
68e34e7f01ab cleanup "simple" type encodings
blanchet
parents: 44738
diff changeset
   633
           (case (poly, level) of
68e34e7f01ab cleanup "simple" type encodings
blanchet
parents: 44738
diff changeset
   634
              (Polymorphic, All_Types) =>
68e34e7f01ab cleanup "simple" type encodings
blanchet
parents: 44738
diff changeset
   635
              Simple_Types (First_Order, Polymorphic, All_Types)
68e34e7f01ab cleanup "simple" type encodings
blanchet
parents: 44738
diff changeset
   636
            | (Mangled_Monomorphic, _) =>
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   637
              if granularity_of_type_level level = All_Vars then
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   638
                Simple_Types (First_Order, Mangled_Monomorphic, level)
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   639
              else
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   640
                raise Same.SAME
44742
68e34e7f01ab cleanup "simple" type encodings
blanchet
parents: 44738
diff changeset
   641
            | _ => raise Same.SAME)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   642
         | ("simple_higher", (SOME poly, _)) =>
44591
0b107d11f634 extended simple types with polymorphism -- the implementation still needs some work though
blanchet
parents: 44589
diff changeset
   643
           (case (poly, level) of
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   644
              (Polymorphic, All_Types) =>
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   645
              Simple_Types (Higher_Order, Polymorphic, All_Types)
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   646
            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
44742
68e34e7f01ab cleanup "simple" type encodings
blanchet
parents: 44738
diff changeset
   647
            | (Mangled_Monomorphic, _) =>
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   648
              if granularity_of_type_level level = All_Vars then
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   649
                Simple_Types (Higher_Order, Mangled_Monomorphic, level)
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   650
              else
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   651
                raise Same.SAME
44742
68e34e7f01ab cleanup "simple" type encodings
blanchet
parents: 44738
diff changeset
   652
            | _ => raise Same.SAME)
44810
c1c05a578c1a stricted type encoding parsing
blanchet
parents: 44786
diff changeset
   653
         | ("guards", (SOME poly, _)) =>
45949
70b9d1e9fddc killed "guard@?" encodings -- they were found to be unsound
blanchet
parents: 45948
diff changeset
   654
           if poly = Mangled_Monomorphic andalso
70b9d1e9fddc killed "guard@?" encodings -- they were found to be unsound
blanchet
parents: 45948
diff changeset
   655
              granularity_of_type_level level = Ghost_Type_Arg_Vars then
70b9d1e9fddc killed "guard@?" encodings -- they were found to be unsound
blanchet
parents: 45948
diff changeset
   656
             raise Same.SAME
70b9d1e9fddc killed "guard@?" encodings -- they were found to be unsound
blanchet
parents: 45948
diff changeset
   657
           else
70b9d1e9fddc killed "guard@?" encodings -- they were found to be unsound
blanchet
parents: 45948
diff changeset
   658
             Guards (poly, level)
44810
c1c05a578c1a stricted type encoding parsing
blanchet
parents: 44786
diff changeset
   659
         | ("tags", (SOME poly, _)) =>
45949
70b9d1e9fddc killed "guard@?" encodings -- they were found to be unsound
blanchet
parents: 45948
diff changeset
   660
           if granularity_of_type_level level = Ghost_Type_Arg_Vars then
70b9d1e9fddc killed "guard@?" encodings -- they were found to be unsound
blanchet
parents: 45948
diff changeset
   661
             raise Same.SAME
70b9d1e9fddc killed "guard@?" encodings -- they were found to be unsound
blanchet
parents: 45948
diff changeset
   662
           else
70b9d1e9fddc killed "guard@?" encodings -- they were found to be unsound
blanchet
parents: 45948
diff changeset
   663
             Tags (poly, level)
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   664
         | ("args", (SOME poly, All_Types (* naja *))) =>
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   665
           Guards (poly, Const_Arg_Types)
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   666
         | ("erased", (NONE, All_Types (* naja *))) =>
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   667
           Guards (Polymorphic, No_Types)
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
   668
         | _ => raise Same.SAME)
44785
f4975fa4a2f8 parse new experimental '@' encodings
blanchet
parents: 44783
diff changeset
   669
  handle Same.SAME => error ("Unknown type encoding: " ^ 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
   670
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   671
fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   672
                    (Simple_Types (order, _, level)) =
44591
0b107d11f634 extended simple types with polymorphism -- the implementation still needs some work though
blanchet
parents: 44589
diff changeset
   673
    Simple_Types (order, Mangled_Monomorphic, level)
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   674
  | adjust_type_enc (THF _) type_enc = type_enc
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   675
  | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
44591
0b107d11f634 extended simple types with polymorphism -- the implementation still needs some work though
blanchet
parents: 44589
diff changeset
   676
    Simple_Types (First_Order, Mangled_Monomorphic, level)
45303
bd03b08161ac added DFG unsorted support (like in the old days)
blanchet
parents: 45301
diff changeset
   677
  | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 45299
diff changeset
   678
    Simple_Types (First_Order, Mangled_Monomorphic, level)
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   679
  | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
44591
0b107d11f634 extended simple types with polymorphism -- the implementation still needs some work though
blanchet
parents: 44589
diff changeset
   680
    Simple_Types (First_Order, poly, level)
0b107d11f634 extended simple types with polymorphism -- the implementation still needs some work though
blanchet
parents: 44589
diff changeset
   681
  | adjust_type_enc format (Simple_Types (_, poly, level)) =
44768
a7bc1bdb8bb4 rationalize uniform encodings
blanchet
parents: 44754
diff changeset
   682
    adjust_type_enc format (Guards (poly, level))
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44410
diff changeset
   683
  | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44410
diff changeset
   684
    (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44410
diff changeset
   685
  | adjust_type_enc _ type_enc = type_enc
43101
1d46d85cd78b make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents: 43098
diff changeset
   686
45509
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   687
fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   688
  | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   689
  | constify_lifted (Free (x as (s, _))) =
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   690
    (if String.isPrefix lam_lifted_prefix s then Const else Free) x
45509
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   691
  | constify_lifted t = t
624872fc47bf use consts, not frees, for lambda-lifting
blanchet
parents: 45508
diff changeset
   692
46375
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   693
(* Requires bound variables not to clash with any schematic variables (as should
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   694
   be the case right after lambda-lifting). *)
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   695
fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   696
    let
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   697
      val names = Name.make_context (map fst (Term.add_var_names t []))
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   698
      val (s, _) = Name.variant s names
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   699
    in open_form (subst_bound (Var ((s, 0), T), t)) end
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   700
  | open_form t = t
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   701
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   702
fun lift_lams_part_1 ctxt type_enc =
45568
211a6e6cbc04 move eta-contraction to before translation to Metis, to ensure everything stays in sync
blanchet
parents: 45565
diff changeset
   703
  map close_form #> rpair ctxt
44088
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   704
  #-> Lambda_Lifting.lift_lambdas
45564
2231a151db59 protect prefix against variant mutations
blanchet
parents: 45554
diff changeset
   705
          (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
2231a151db59 protect prefix against variant mutations
blanchet
parents: 45554
diff changeset
   706
                    lam_lifted_poly_prefix
2231a151db59 protect prefix against variant mutations
blanchet
parents: 45554
diff changeset
   707
                  else
2231a151db59 protect prefix against variant mutations
blanchet
parents: 45554
diff changeset
   708
                    lam_lifted_mono_prefix) ^ "_a"))
44088
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   709
          Lambda_Lifting.is_quantifier
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   710
  #> fst
46375
d724066ff3d0 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
blanchet
parents: 46371
diff changeset
   711
val lift_lams_part_2 = pairself (map (open_form o constify_lifted))
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 45551
diff changeset
   712
val lift_lams = lift_lams_part_2 ooo lift_lams_part_1
44088
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   713
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   714
fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   715
    intentionalize_def t
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   716
  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   717
    let
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   718
      fun lam T t = Abs (Name.uu, T, t)
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   719
      val (head, args) = strip_comb t ||> rev
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   720
      val head_T = fastype_of head
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   721
      val n = length args
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   722
      val arg_Ts = head_T |> binder_types |> take n |> rev
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   723
      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   724
    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   725
  | intentionalize_def t = t
3693baa6befb move lambda-lifting code to ATP encoding, so it can be used by Metis
blanchet
parents: 44003
diff changeset
   726
40114
blanchet
parents: 40069
diff changeset
   727
type translated_formula =
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   728
  {name : string,
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46339
diff changeset
   729
   stature : stature,
43496
92f5a4c78b37 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents: 43495
diff changeset
   730
   kind : formula_kind,
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   731
   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
   732
   atomic_types : typ list}
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   733
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46339
diff changeset
   734
fun update_iformula f ({name, stature, kind, iformula, atomic_types}
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   735
                       : translated_formula) =
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46339
diff changeset
   736
  {name = name, stature = stature, kind = kind, iformula = f iformula,
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   737
   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
   738
43859
b7890554c424 renamed internal data structure
blanchet
parents: 43858
diff changeset
   739
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
   740
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
   741
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
   742
  let val T = get_T x in
44399
cd1e32b8d4c4 added caching for (in)finiteness checks
blanchet
parents: 44398
diff changeset
   743
    if exists (type_instance ctxt T o get_T) xs then xs
cd1e32b8d4c4 added caching for (in)finiteness checks
blanchet
parents: 44398
diff changeset
   744
    else x :: filter_out (type_generalization ctxt T o get_T) xs
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
   745
  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
   746
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
   747
(* 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
   748
datatype type_arg_policy =
45937
blanchet
parents: 45920
diff changeset
   749
  Explicit_Type_Args of bool (* infer_from_term_args *) |
44771
0e5d4388bbac make mangling sound w.r.t. type arguments
blanchet
parents: 44770
diff changeset
   750
  Mangled_Type_Args |
42753
c9552e617acc drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents: 42750
diff changeset
   751
  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
   752
45945
aa8100cc02dc no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents: 45939
diff changeset
   753
fun type_arg_policy monom_constrs type_enc s =
45315
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   754
  let val poly = polymorphism_of_type_enc type_enc in
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   755
    if s = type_tag_name then
45315
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   756
      if poly = Mangled_Monomorphic then Mangled_Type_Args
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   757
      else Explicit_Type_Args false
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   758
    else case type_enc of
45315
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   759
      Simple_Types (_, Polymorphic, _) => Explicit_Type_Args false
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   760
    | Tags (_, All_Types) => No_Type_Args
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   761
    | _ =>
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   762
      let val level = level_of_type_enc type_enc in
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   763
        if level = No_Types orelse s = @{const_name HOL.eq} orelse
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   764
           (s = app_op_name andalso level = Const_Arg_Types) then
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   765
          No_Type_Args
45315
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   766
        else if poly = Mangled_Monomorphic then
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   767
          Mangled_Type_Args
45945
aa8100cc02dc no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents: 45939
diff changeset
   768
        else if member (op =) monom_constrs s andalso
aa8100cc02dc no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents: 45939
diff changeset
   769
                granularity_of_type_level level = Positively_Naked_Vars then
aa8100cc02dc no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents: 45939
diff changeset
   770
          No_Type_Args
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   771
        else
44811
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   772
          Explicit_Type_Args
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   773
              (level = All_Types orelse
0bff1a4228b3 started work on ghost type arg encoding
blanchet
parents: 44810
diff changeset
   774
               granularity_of_type_level level = Ghost_Type_Arg_Vars)
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   775
      end
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   776
  end
42227
662b50b7126f if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents: 42180
diff changeset
   777
44625
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   778
(* Make atoms for sorted type variables. *)
43263
blanchet
parents: 43259
diff changeset
   779
fun generic_add_sorts_on_type (_, []) = I
blanchet
parents: 43259
diff changeset
   780
  | generic_add_sorts_on_type ((x, i), s :: ss) =
blanchet
parents: 43259
diff changeset
   781
    generic_add_sorts_on_type ((x, i), ss)
blanchet
parents: 43259
diff changeset
   782
    #> (if s = the_single @{sort HOL.type} then
43093
blanchet
parents: 43092
diff changeset
   783
          I
blanchet
parents: 43092
diff changeset
   784
        else if i = ~1 then
44623
blanchet
parents: 44622
diff changeset
   785
          insert (op =) (`make_type_class s, `make_fixed_type_var x)
43093
blanchet
parents: 43092
diff changeset
   786
        else
44623
blanchet
parents: 44622
diff changeset
   787
          insert (op =) (`make_type_class s,
blanchet
parents: 44622
diff changeset
   788
                         (make_schematic_type_var (x, i), x)))
43263
blanchet
parents: 43259
diff changeset
   789
fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
blanchet
parents: 43259
diff changeset
   790
  | add_sorts_on_tfree _ = I
blanchet
parents: 43259
diff changeset
   791
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
blanchet
parents: 43259
diff changeset
   792
  | add_sorts_on_tvar _ = I
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   793
44625
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   794
fun type_class_formula type_enc class arg =
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   795
  AAtom (ATerm (class, arg ::
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   796
      (case type_enc of
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   797
         Simple_Types (First_Order, Polymorphic, _) =>
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 45299
diff changeset
   798
         if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44742
diff changeset
   799
         else []
44625
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   800
       | _ => [])))
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   801
fun formulas_for_types type_enc add_sorts_on_typ Ts =
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   802
  [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
44625
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   803
     |> map (fn (class, name) =>
4a1132815a70 more tuning
blanchet
parents: 44624
diff changeset
   804
                type_class_formula type_enc class (ATerm (name, [])))
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
   805
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
   806
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
   807
  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
   808
    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
   809
  end
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
   810
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
   811
  | 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
   812
fun mk_aquant _ [] phi = phi
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   813
  | 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
   814
    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
   815
  | 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
   816
45315
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   817
fun close_universally add_term_vars phi =
41145
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   818
  let
45315
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   819
    fun add_formula_vars bounds (AQuant (_, xs, phi)) =
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   820
        add_formula_vars (map fst xs @ bounds) phi
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   821
      | add_formula_vars bounds (AConn (_, phis)) =
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   822
        fold (add_formula_vars bounds) phis
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   823
      | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   824
  in mk_aquant AForall (add_formula_vars [] phi []) phi end
42522
413b56894f82 close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents: 42521
diff changeset
   825
45377
blanchet
parents: 45364
diff changeset
   826
fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
blanchet
parents: 45364
diff changeset
   827
    (if is_tptp_variable s andalso
blanchet
parents: 45364
diff changeset
   828
        not (String.isPrefix tvar_prefix s) andalso
blanchet
parents: 45364
diff changeset
   829
        not (member (op =) bounds name) then
blanchet
parents: 45364
diff changeset
   830
       insert (op =) (name, NONE)
blanchet
parents: 45364
diff changeset
   831
     else
blanchet
parents: 45364
diff changeset
   832
       I)
blanchet
parents: 45364
diff changeset
   833
    #> fold (add_term_vars bounds) tms
blanchet
parents: 45364
diff changeset
   834
  | add_term_vars bounds (AAbs ((name, _), tm)) =
blanchet
parents: 45364
diff changeset
   835
    add_term_vars (name :: bounds) tm
45401
36478a5f6104 made SML/NJ happy
blanchet
parents: 45377
diff changeset
   836
fun close_formula_universally phi = close_universally add_term_vars phi
45315
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   837
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   838
fun add_iterm_vars bounds (IApp (tm1, tm2)) =
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   839
    fold (add_iterm_vars bounds) [tm1, tm2]
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   840
  | add_iterm_vars _ (IConst _) = I
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   841
  | add_iterm_vars bounds (IVar (name, T)) =
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   842
    not (member (op =) bounds name) ? insert (op =) (name, SOME T)
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   843
  | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
dfbbc5ac7194 improved TFF1 output
blanchet
parents: 45304
diff changeset
   844
fun close_iformula_universally phi = close_universally add_iterm_vars phi
41145
a5ee3b8e5a90 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents: 41140
diff changeset
   845
46338
b02ff6b17599 better handling of individual type for DFG format (SPASS)
blanchet
parents: 46320
diff changeset
   846
val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
44594
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   847
val fused_infinite_type = Type (fused_infinite_type_name, [])
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   848
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   849
fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   850
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
   851
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
   852
  let
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   853
    fun term (Type (s, Ts)) =
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   854
      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
   855
               (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
   856
             | (true, @{type_name fun}) => `I tptp_fun_type
44594
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   857
             | _ => if s = fused_infinite_type_name andalso
44235
85e9dad3c187 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
blanchet
parents: 44121
diff changeset
   858
                       is_format_typed format then
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
   859
                      `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
   860
                    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
   861
                      `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
   862
             map term Ts)
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   863
    | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
44594
ae82943481e9 added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents: 44593
diff changeset
   864
    | term (TVar (x, _)) = ATerm (tvar_name x, [])
42994
fe291ab75eb5 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents: 42966
diff changeset
   865
  in term end
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   866
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
   867
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
   868
  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
   869
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   870
(* 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
   871
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
   872
42562
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   873
fun generic_mangled_type_name f (ATerm (name, [])) = f name
f1d903f789b1 killed needless datatype "combtyp" in Metis
blanchet
parents: 42561
diff changeset
   874
  | 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
   875
    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
   876
    ^ ")"
43692
264881a20f50 make SML/NJ happy + tuning
blanchet
parents: 43678
diff changeset
   877
  | 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
   878
44396
66b9b3fcd608 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
blanchet
parents: 44394
diff changeset
   879
fun mangled_type format type_enc =
66b9b3fcd608 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
blanchet
parents: 44394
diff changeset
   880
  generic_mangled_type_name fst o ho_term_from_typ format type_enc
66b9b3fcd608 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
blanchet
parents: 44394
diff changeset
   881
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   882
fun make_simple_type s =
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   883
  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
   884
     s = tptp_individual_type then
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   885
    s
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   886
  else
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   887
    simple_type_prefix ^ ascii_of s
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
   888
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
   889
fun ho_type_from_ho_term type_enc pred_sym ary =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   890
  let
44593
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44591
diff changeset
   891
    fun to_mangled_atype ty =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   892
      AType ((make_simple_type (generic_mangled_type_name fst ty),
44593
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44591
diff changeset
   893
              generic_mangled_type_name snd ty), [])
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44591
diff changeset
   894
    fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44591
diff changeset
   895
      | to_poly_atype _ = raise Fail "unexpected type abstraction"
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44591
diff changeset
   896
    val to_atype =
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44591
diff changeset
   897
      if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
ccf40af26ae9 implement more of the polymorphic simply typed format TFF(1)
blanchet
parents: 44591
diff changeset
   898
      else to_mangled_atype
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   899
    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
   900
    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
   901
      | 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
   902
      | 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
   903
    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
   904
        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
   905
      | to_ho _ = raise Fail "unexpected type abstraction"
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   906
  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
   907
43677
2cd0b478d1b6 added generation of lambdas in THF
nik
parents: 43676
diff changeset
   908
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
   909
  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
   910
  o ho_term_from_typ format type_enc
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   911
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   912
fun mangled_const_name format type_enc T_args (s, s') =
42963
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   913
  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
   914
    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
   915
    fun type_suffix f g =
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   916
      fold_rev (curry (op ^) o g o prefix mangled_type_sep
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   917
                o generic_mangled_type_name f) ty_args ""
5725deb11ae7 identify HOL functions with THF functions
blanchet
parents: 42962
diff changeset
   918
  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
   919
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
   920
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
   921
  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
   922
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
   923
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
   924
  (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
   925
   -- 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
   926
                    [] >> 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
   927
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
   928
  (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
   929
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
   930
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
   931
  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
   932
    |> 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
   933
           (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
   934
                                                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
   935
    |> 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
   936
42561
23ddc4e3d19c have properly type-instantiated helper facts (combinators and If)
blanchet
parents: 42560
diff changeset
   937
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
   938
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
   939
  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
   940
    (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
   941
  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
   942
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
   943
fun introduce_proxies_in_iterm type_enc =
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   944
  let
43987
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   945
    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
   946
      | 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
   947
                       _ =
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   948
        (* 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
   949
           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
   950
           "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
   951
           possible. *)
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   952
        IAbs ((`I "P", p_T),
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   953
              IApp (IConst (`I ho_quant, T, []),
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   954
                    IAbs ((`I "X", x_T),
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   955
                          IApp (IConst (`I "P", p_T, []),
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   956
                                IConst (`I "X", x_T, [])))))
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   957
      | 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
   958
    fun intro top_level args (IApp (tm1, tm2)) =
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   959
        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
   960
      | 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
   961
        (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
   962
           SOME proxy_base =>
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43624
diff changeset
   963
           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
   964
             case (top_level, s) of
43987
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   965
               (_, "c_False") => IConst (`I tptp_false, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   966
             | (_, "c_True") => IConst (`I tptp_true, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   967
             | (false, "c_Not") => IConst (`I tptp_not, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   968
             | (false, "c_conj") => IConst (`I tptp_and, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   969
             | (false, "c_disj") => IConst (`I tptp_or, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   970
             | (false, "c_implies") => IConst (`I tptp_implies, T, [])
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   971
             | (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
   972
             | (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
   973
             | (false, s) =>
44097
3cae91385086 workaround THF parser limitation
blanchet
parents: 44088
diff changeset
   974
               if is_tptp_equal s andalso length args = 2 then
3cae91385086 workaround THF parser limitation
blanchet
parents: 44088
diff changeset
   975
                 IConst (`I tptp_equal, T, [])
3cae91385086 workaround THF parser limitation
blanchet
parents: 44088
diff changeset
   976
               else
44589
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44587
diff changeset
   977
                 (* Use a proxy even for partially applied THF0 equality,
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44587
diff changeset
   978
                    because the LEO-II and Satallax parsers complain about not
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44587
diff changeset
   979
                    being able to infer the type of "=". *)
44097
3cae91385086 workaround THF parser limitation
blanchet
parents: 44088
diff changeset
   980
                 IConst (proxy_base |>> prefix const_prefix, T, T_args)
43987
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   981
             | _ => IConst (name, T, [])
42569
5737947e4c77 make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents: 42568
diff changeset
   982
           else
43987
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   983
             IConst (proxy_base |>> prefix const_prefix, T, T_args)
45167
6bc8d260d459 gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
blanchet
parents: 44859
diff changeset
   984
          | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
6bc8d260d459 gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
blanchet
parents: 44859
diff changeset
   985
                    else IConst (name, T, T_args))
43987
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   986
      | 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
   987
      | intro _ _ tm = tm
2850b7dc27a4 further worked around LEO-II parser limitation, with eta-expansion
blanchet
parents: 43985
diff changeset
   988
  in intro true [] end
42568
7b9801a34836 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents: 42566
diff changeset
   989
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   990
fun mangle_type_args_in_iterm format type_enc =
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   991
  if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   992
    let
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   993
      fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   994
        | mangle (tm as IConst (_, _, [])) = tm
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   995
        | mangle (tm as IConst (name as (s, _), T, T_args)) =
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45509
diff changeset
   996
          (case unprefix_and_unascii const_prefix s of
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   997
             NONE => tm
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
   998
           | SOME s'' =>
45945
aa8100cc02dc no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents: 45939
diff changeset
   999
             case type_arg_policy [] type_enc (invert_const s'') of
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1000
               Mangled_Type_Args =>
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1001
               IConst (mangled_const_name format type_enc T_args name, T, [])
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1002
             | _ => tm)
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1003
        | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1004
        | mangle tm = tm
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1005
    in mangle end
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1006
  else
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1007
    I
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1008
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1009
fun chop_fun 0 T = ([], T)
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1010
  | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1011
    chop_fun (n - 1) ran_T |>> cons dom_T
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1012
  | chop_fun _ T = ([], T)
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1013
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1014
fun filter_const_type_args _ _ _ [] = []
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1015
  | filter_const_type_args thy s ary T_args =
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1016
    let
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1017
      val U = robust_const_type thy s
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1018
      val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1019
      val U_args = (s, U) |> robust_const_typargs thy
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1020
    in
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1021
      U_args ~~ T_args
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1022
      |> map (fn (U, T) =>
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1023
                 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1024
    end
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1025
    handle TYPE _ => T_args
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1026
45945
aa8100cc02dc no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents: 45939
diff changeset
  1027
fun filter_type_args_in_iterm thy monom_constrs type_enc =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1028
  let
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1029
    fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1030
      | filt _ (tm as IConst (_, _, [])) = tm
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1031
      | filt ary (IConst (name as (s, _), T, T_args)) =
45511
9b0f8ca4388e continued implementation of lambda-lifting in Metis
blanchet
parents: 45509
diff changeset
  1032
        (case unprefix_and_unascii const_prefix s of
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1033
           NONE =>
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1034
           (name,
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1035
            if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1036
              []
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1037
            else
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1038
              T_args)
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1039
         | SOME s'' =>
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1040
           let
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1041
             val s'' = invert_const s''
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1042
             fun filter_T_args false = T_args
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1043
               | filter_T_args true = filter_const_type_args thy s'' ary T_args
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1044
           in
45945
aa8100cc02dc no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents: 45939
diff changeset
  1045
             case type_arg_policy monom_constrs type_enc s'' of
45937
blanchet
parents: 45920
diff changeset
  1046
               Explicit_Type_Args infer_from_term_args =>
blanchet
parents: 45920
diff changeset
  1047
               (name, filter_T_args infer_from_term_args)
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1048
             | No_Type_Args => (name, [])
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1049
             | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1050
           end)
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1051
        |> (fn (name, T_args) => IConst (name, T, T_args))
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1052
      | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1053
      | filt _ tm = tm
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1054
  in filt 0 end
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1055
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1056
fun iformula_from_prop ctxt format type_enc eq_as_iff =
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1057
  let
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1058
    val thy = Proof_Context.theory_of ctxt
45316
08d84bdd5b37 improve handling of bound type variables (esp. for TFF1)
blanchet
parents: 45315
diff changeset
  1059
    fun do_term bs t atomic_Ts =
44495
4c2242c8a96c added choice operator output for
nik
parents: 44494
diff changeset
  1060
      iterm_from_term thy format bs (Envir.eta_contract t)
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1061
      |>> (introduce_proxies_in_iterm type_enc
44774
72785558a6ff separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents: 44773
diff changeset
  1062
           #> mangle_type_args_in_iterm format type_enc
44773
e701dabbfe37 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents: 44772
diff changeset
  1063
           #> AAtom)
45316
08d84bdd5b37 improve handling of bound type variables (esp. for TFF1)
blanchet
parents: 45315
diff changeset
  1064
      ||> union (op =) atomic_Ts
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1065
    fun do_quant bs q pos s T t' =
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1066
      let
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1067
        val s = singleton (Name.variant_list (map fst bs)) s
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1068
        val universal = Option.map (q = AExists ? not) pos
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1069
        val name =
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1070
          s |> `(case universal of
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1071
                   SOME true => make_all_bound_var
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1072
                 | SOME false => make_exist_bound_var
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1073
                 | NONE => make_bound_var)
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1074
      in
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1075
        do_formula ((s, (name, T)) :: bs) pos t'
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1076
        #>> mk_aquant q [(name, SOME T)]
45316
08d84bdd5b37 improve handling of bound type variables (esp. for TFF1)
blanchet
parents: 45315
diff changeset
  1077
        ##> union (op =) (atomic_types_of T)
38518
54727b44e277 handle bound name conflicts gracefully in FOF translation
blanchet
parents: 38496
diff changeset
  1078
      end
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1079
    and do_conn bs c pos1 t1 pos2 t2 =
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1080
      do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1081
    and do_formula bs pos t =
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1082
      case t of
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1083
        @{const Trueprop} $ t1 => do_formula bs pos t1
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1084
      | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1085
      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1086
        do_quant bs AForall pos s T t'
45167
6bc8d260d459 gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
blanchet
parents: 44859
diff changeset
  1087
      | (t0 as Const (@{const_name All}, _)) $ t1 =>
6bc8d260d459 gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
blanchet
parents: 44859
diff changeset
  1088
        do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1089
      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1090
        do_quant bs AExists pos s T t'
45167
6bc8d260d459 gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
blanchet
parents: 44859
diff changeset
  1091
      | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
6bc8d260d459 gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
blanchet
parents: 44859
diff changeset
  1092
        do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1093
      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1094
      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1095
      | @{const HOL.implies} $ t1 $ t2 =>
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1096
        do_conn bs AImplies (Option.map not pos) t1 pos t2
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
  1097
      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
44403
15160cdc4688 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents: 44402
diff changeset
  1098
        if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
  1099
      | _ => do_term bs t
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1100
  in do_formula [] end
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1101
46093
blanchet
parents: 46071
diff changeset
  1102
fun presimplify_term ctxt t =
blanchet
parents: 46071
diff changeset
  1103
  t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
blanchet
parents: 46071
diff changeset
  1104
       ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
blanchet
parents: 46071
diff changeset
  1105
          #> Meson.presimplify
blanchet
parents: 46071
diff changeset
  1106
          #> prop_of)
38282
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1107
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
  1108
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
  1109
fun conceal_bounds Ts t =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1110
  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
  1111
                    (0 upto length Ts - 1 ~~ Ts), t)
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1112
fun reveal_bounds Ts =
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1113
  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
  1114
                    (0 upto length Ts - 1 ~~ Ts))
319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff changeset
  1115
43265
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1116
fun is_fun_equality (@{const_name HOL.eq},
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1117
                     Type (_, [Type (@{type_name fun}, _), _])) = true
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1118
  | is_fun_equality _ = false
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1119
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
  1120
fun extensionalize_term ctxt t =
43265
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1121
  if exists_Const is_fun_equality t then
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1122
    let val thy = Proof_Context.theory_of ctxt in
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1123
      t |> cterm_of thy |> Meson.extensionalize_conv ctxt
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1124
        |> prop_of |> Logic.dest_equals |> snd
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1125
    end
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1126
  else
096237fe70f1 don't needlessly extensionalize
blanchet
parents: 43264
diff changeset
  1127
    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
  1128
43862
a14fdb8c0497 pass kind to lambda-translation function
blanchet
parents: 43861
diff changeset
  1129
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
  1130
  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
  1131
    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
  1132
      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
  1133
    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
  1134
      let
44814
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1135
        fun trans Ts 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
  1136
          case t of
44814
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1137
            @{const Not} $ t1 => @{const Not} $ trans Ts t1
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
  1138
          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
44814
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1139
            t0 $ Abs (s, T, trans (T :: Ts) 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
  1140
          | (t0 as Const (@{const_name All}, _)) $ t1 =>
44814
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1141
            trans Ts (t0 $ eta_expand Ts t1 1)
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
  1142
          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
44814
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1143
            t0 $ Abs (s, T, trans (T :: Ts) 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
  1144
          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
44814
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1145
            trans Ts (t0 $ eta_expand Ts t1 1)
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1146
          | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1147
            t0 $ trans Ts t1 $ trans Ts t2
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1148
          | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1149
            t0 $ trans Ts t1 $ trans Ts t2
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1150
          | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1151
            t0 $ trans Ts t1 $ trans Ts t2
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
  1152
          | (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
  1153
              $ t1 $ t2 =>
44814
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1154
            t0 $ trans Ts t1 $ trans Ts t2
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
  1155
          | _ =>
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
  1156
            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
  1157
            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
  1158
        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
44814
52318464c73b also implemented ghost version of the tagged encodings
blanchet
parents: 44812
diff changeset
  1159
      in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
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
  1160
  end
43856
d636b053d4ff move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents: 43830
diff changeset
  1161
43997
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
  1162
fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
  1163
    do_cheaply_conceal_lambdas Ts t1
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
  1164
    $ do_cheaply_conceal_lambdas Ts t2
578460971517 fixed lambda concealing
blanchet
parents: 43989
diff changeset
  1165
  | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
45554
09ad83de849c don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents: 4555