author  blanchet 
Sun, 17 Jul 2011 14:11:35 +0200  
changeset 43858  be41d12de6fa 
parent 43857  a875729380a4 
child 43859  b7890554c424 
permissions  rwrr 
43283  1 
(* Title: HOL/Tools/ATP/atp_translate.ML 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

2 
Author: Fabian Immler, TU Muenchen 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

3 
Author: Makarius 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

4 
Author: Jasmin Blanchette, TU Muenchen 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

5 

39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39452
diff
changeset

6 
Translation of HOL to FOL for Sledgehammer. 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

7 
*) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

8 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

9 
signature ATP_TRANSLATE = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

10 
sig 
43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

11 
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43130
diff
changeset

12 
type connective = ATP_Problem.connective 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43130
diff
changeset

13 
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula 
42939  14 
type format = ATP_Problem.format 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

15 
type formula_kind = ATP_Problem.formula_kind 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

16 
type 'a problem = 'a ATP_Problem.problem 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

17 

43421  18 
datatype locality = 
19 
General  Helper  Extensionality  Intro  Elim  Simp  Local  Assum  

20 
Chained 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

21 

43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

22 
datatype order = First_Order  Higher_Order 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

23 
datatype polymorphism = Polymorphic  Monomorphic  Mangled_Monomorphic 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

24 
datatype type_level = 
43362  25 
All_Types  Noninf_Nonmono_Types  Fin_Nonmono_Types  Const_Arg_Types  
26 
No_Types 

43128  27 
datatype type_heaviness = Heavyweight  Lightweight 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

28 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

29 
datatype type_enc = 
43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

30 
Simple_Types of order * type_level  
42837  31 
Preds of polymorphism * type_level * type_heaviness  
32 
Tags of polymorphism * type_level * type_heaviness 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

33 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

34 
val bound_var_prefix : string 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

35 
val schematic_var_prefix : string 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

36 
val fixed_var_prefix : string 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

37 
val tvar_prefix : string 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

38 
val tfree_prefix : string 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

39 
val const_prefix : string 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

40 
val type_const_prefix : string 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

41 
val class_prefix : string 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

42 
val skolem_const_prefix : string 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

43 
val old_skolem_const_prefix : string 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

44 
val new_skolem_const_prefix : string 
43125
ddf63baabdec
distinguish different kinds of typing informations in the fact name
blanchet
parents:
43121
diff
changeset

45 
val type_decl_prefix : string 
ddf63baabdec
distinguish different kinds of typing informations in the fact name
blanchet
parents:
43121
diff
changeset

46 
val sym_decl_prefix : string 
ddf63baabdec
distinguish different kinds of typing informations in the fact name
blanchet
parents:
43121
diff
changeset

47 
val preds_sym_formula_prefix : string 
43129  48 
val lightweight_tags_sym_formula_prefix : string 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

49 
val fact_prefix : string 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

50 
val conjecture_prefix : string 
42881
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

51 
val helper_prefix : string 
43125
ddf63baabdec
distinguish different kinds of typing informations in the fact name
blanchet
parents:
43121
diff
changeset

52 
val class_rel_clause_prefix : string 
ddf63baabdec
distinguish different kinds of typing informations in the fact name
blanchet
parents:
43121
diff
changeset

53 
val arity_clause_prefix : string 
ddf63baabdec
distinguish different kinds of typing informations in the fact name
blanchet
parents:
43121
diff
changeset

54 
val tfree_clause_prefix : string 
42881
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

55 
val typed_helper_suffix : string 
43125
ddf63baabdec
distinguish different kinds of typing informations in the fact name
blanchet
parents:
43121
diff
changeset

56 
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

57 
val type_tag_idempotence_helper_name : string 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

58 
val predicator_name : string 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

59 
val app_op_name : string 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43102
diff
changeset

60 
val type_tag_name : string 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

61 
val type_pred_name : string 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

62 
val simple_type_prefix : string 
43174  63 
val prefixed_predicator_name : string 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

64 
val prefixed_app_op_name : string 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

65 
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

66 
val ascii_of : string > string 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

67 
val unascii_of : string > string 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

68 
val strip_prefix_and_unascii : string > string > string option 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

69 
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

70 
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

71 
val invert_const : string > string 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

72 
val unproxify_const : string > string 
43093  73 
val new_skolem_var_name_from_const : string > string 
74 
val num_type_args : theory > string > int 

43248
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

75 
val atp_irrelevant_consts : string list 
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

76 
val atp_schematic_consts_of : term > typ list Symtab.table 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

77 
val is_locality_global : locality > bool 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

78 
val type_enc_from_string : string > type_enc 
43828
e07a2c4cbad8
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
blanchet
parents:
43827
diff
changeset

79 
val is_type_enc_higher_order : type_enc > bool 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

80 
val polymorphism_of_type_enc : type_enc > polymorphism 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

81 
val level_of_type_enc : type_enc > type_level 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

82 
val is_type_enc_virtually_sound : type_enc > bool 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

83 
val is_type_enc_fairly_sound : type_enc > bool 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

84 
val choose_format : format list > type_enc > format * type_enc 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43130
diff
changeset

85 
val mk_aconns : 
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43130
diff
changeset

86 
connective > ('a, 'b, 'c) formula list > ('a, 'b, 'c) formula 
43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

87 
val unmangled_const : string > string * (string, 'b) ho_term list 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

88 
val unmangled_const_name : string > string 
43194  89 
val helper_table : ((string * bool) * thm list) list 
43501
0e422a84d0b2
don't change the way helpers are generated for the exporter's sake
blanchet
parents:
43496
diff
changeset

90 
val factsN : string 
43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

91 
val conceal_lambdas : Proof.context > term > term 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

92 
val introduce_combinators : Proof.context > term > term 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39975
diff
changeset

93 
val prepare_atp_problem : 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

94 
Proof.context > format > formula_kind > formula_kind > type_enc > bool 
43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

95 
> bool > (term list > term list) > bool > bool > term list > term 
43304
6901ebafbb8d
cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
blanchet
parents:
43297
diff
changeset

96 
> ((string * locality) * term) list 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42540
diff
changeset

97 
> string problem * string Symtab.table * int * int 
43214  98 
* (string * locality) list vector * int list * int Symtab.table 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

99 
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

100 
end; 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

101 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

102 
structure ATP_Translate : ATP_TRANSLATE = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

103 
struct 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

104 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

105 
open ATP_Util 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

106 
open ATP_Problem 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

107 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

108 
type name = string * string 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

109 

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

110 
val generate_info = false (* experimental *) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

111 

43693  112 
fun isabelle_info s = 
113 
if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) 

114 
else NONE 

42879  115 

43693  116 
val introN = "intro" 
117 
val elimN = "elim" 

118 
val simpN = "simp" 

42879  119 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

120 
val bound_var_prefix = "B_" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

121 
val schematic_var_prefix = "V_" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

122 
val fixed_var_prefix = "v_" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

123 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

124 
val tvar_prefix = "T_" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

125 
val tfree_prefix = "t_" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

126 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

127 
val const_prefix = "c_" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

128 
val type_const_prefix = "tc_" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

129 
val class_prefix = "cl_" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

130 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

131 
val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

132 
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

133 
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

134 

42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

135 
val type_decl_prefix = "ty_" 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

136 
val sym_decl_prefix = "sy_" 
43125
ddf63baabdec
distinguish different kinds of typing informations in the fact name
blanchet
parents:
43121
diff
changeset

137 
val preds_sym_formula_prefix = "psy_" 
43129  138 
val lightweight_tags_sym_formula_prefix = "tsy_" 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

139 
val fact_prefix = "fact_" 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

140 
val conjecture_prefix = "conj_" 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

141 
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

142 
val class_rel_clause_prefix = "clar_" 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

143 
val arity_clause_prefix = "arity_" 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

144 
val tfree_clause_prefix = "tfree_" 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

145 

42881
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

146 
val typed_helper_suffix = "_T" 
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

147 
val untyped_helper_suffix = "_U" 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

148 
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem" 
42881
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

149 

42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

150 
val predicator_name = "hBOOL" 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

151 
val app_op_name = "hAPP" 
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43102
diff
changeset

152 
val type_tag_name = "ti" 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

153 
val type_pred_name = "is" 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

154 
val simple_type_prefix = "ty_" 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

155 

43174  156 
val prefixed_predicator_name = const_prefix ^ predicator_name 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

157 
val prefixed_app_op_name = const_prefix ^ app_op_name 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

158 
val prefixed_type_tag_name = const_prefix ^ type_tag_name 
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

159 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

160 
(* Freshness almost guaranteed! *) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

161 
val sledgehammer_weak_prefix = "Sledgehammer:" 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

162 

43827
62d64709af3b
added option to control which lambda translation to use (for experiments)
blanchet
parents:
43693
diff
changeset

163 
val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_" 
62d64709af3b
added option to control which lambda translation to use (for experiments)
blanchet
parents:
43693
diff
changeset

164 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

165 
(*Escaping of special characters. 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

166 
Alphanumeric characters are left unchanged. 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

167 
The character _ goes to __ 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

168 
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

169 
Other characters go to _nnn where nnn is the decimal ASCII code.*) 
43093  170 
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

171 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

172 
fun stringN_of_int 0 _ = "" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

173 
 stringN_of_int k n = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

174 
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

175 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

176 
fun ascii_of_char c = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

177 
if Char.isAlphaNum c then 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

178 
String.str c 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

179 
else if c = #"_" then 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

180 
"__" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

181 
else if #" " <= c andalso c <= #"/" then 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

182 
"_" ^ 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

183 
else 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

184 
(* fixed width, in case more digits follow *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

185 
"_" ^ stringN_of_int 3 (Char.ord c) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

186 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

187 
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

188 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

189 
(** 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

190 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

191 
(* 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

192 
thread. Also, the errors are impossible. *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

193 
val unascii_of = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

194 
let 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

195 
fun un rcs [] = String.implode(rev rcs) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

196 
 un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

197 
(* 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

198 
 un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

199 
 un rcs (#"_" :: c :: cs) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

200 
if #"A" <= c andalso c<= #"P" then 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

201 
(* translation of #" " to #"/" *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

202 
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

203 
else 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

204 
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

205 
case Int.fromString (String.implode digits) of 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

206 
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

207 
 NONE => un (c :: #"_" :: rcs) cs (* ERROR *) 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

208 
end 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

209 
 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

210 
in un [] o String.explode end 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

211 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

212 
(* 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

213 
unASCII'd. *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

214 
fun strip_prefix_and_unascii s1 s = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

215 
if String.isPrefix s1 s then 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

216 
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

217 
else 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

218 
NONE 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

219 

43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

220 
val proxy_table = 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

221 
[("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

222 
("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

223 
("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

224 
("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

225 
("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

226 
("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

227 
("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

228 
("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

229 
("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

230 
("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

231 
("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

232 
("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

233 
("equal", (@{const_name HOL.eq}, (@{thm fequal_def}, 
43678  234 
("fequal", @{const_name ATP.fequal})))), 
235 
("c_All", (@{const_name All}, (@{thm fAll_def}, 

236 
("fAll", @{const_name ATP.fAll})))), 

237 
("c_Ex", (@{const_name Ex}, (@{thm fEx_def}, 

238 
("fEx", @{const_name ATP.fEx}))))] 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

239 

43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

240 
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

241 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

242 
(* 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

243 
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

244 
val const_trans_table = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

245 
[(@{type_name Product_Type.prod}, "prod"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

246 
(@{type_name Sum_Type.sum}, "sum"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

247 
(@{const_name False}, "False"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

248 
(@{const_name True}, "True"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

249 
(@{const_name Not}, "Not"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

250 
(@{const_name conj}, "conj"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

251 
(@{const_name disj}, "disj"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

252 
(@{const_name implies}, "implies"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

253 
(@{const_name HOL.eq}, "equal"), 
43678  254 
(@{const_name All}, "All"), 
255 
(@{const_name Ex}, "Ex"), 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

256 
(@{const_name If}, "If"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

257 
(@{const_name Set.member}, "member"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

258 
(@{const_name Meson.COMBI}, "COMBI"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

259 
(@{const_name Meson.COMBK}, "COMBK"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

260 
(@{const_name Meson.COMBB}, "COMBB"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

261 
(@{const_name Meson.COMBC}, "COMBC"), 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

262 
(@{const_name Meson.COMBS}, "COMBS")] 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

263 
> Symtab.make 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

264 
> 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

265 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

266 
(* 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

267 
val const_trans_table_inv = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

268 
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

269 
val const_trans_table_unprox = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

270 
Symtab.empty 
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

271 
> 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

272 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

273 
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

274 
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

275 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

276 
fun lookup_const c = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

277 
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

278 
SOME c' => c' 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

279 
 NONE => ascii_of c 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

280 

43622  281 
fun ascii_of_indexname (v, 0) = ascii_of v 
282 
 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

283 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

284 
fun make_bound_var x = bound_var_prefix ^ ascii_of x 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

285 
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

286 
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

287 

43622  288 
fun make_schematic_type_var (x, i) = 
289 
tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) 

290 
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

291 

43622  292 
(* "HOL.eq" is mapped to the ATP's equality. *) 
293 
fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

294 
 make_fixed_const c = const_prefix ^ lookup_const c 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

295 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

296 
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

297 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

298 
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

299 

43093  300 
fun new_skolem_var_name_from_const s = 
301 
let val ss = s > space_explode Long_Name.separator in 

302 
nth ss (length ss  2) 

303 
end 

304 

305 
(* The number of type arguments of a constant, zero if it's monomorphic. For 

306 
(instances of) Skolem pseudoconstants, this information is encoded in the 

307 
constant name. *) 

308 
fun num_type_args thy s = 

309 
if String.isPrefix skolem_const_prefix s then 

310 
s > space_explode Long_Name.separator > List.last > Int.fromString > the 

311 
else 

312 
(s, Sign.the_const_type thy s) > Sign.const_typargs thy > length 

313 

43248
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

314 
(* 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

315 
handled specially via "fFalse", "fTrue", ..., "fequal". *) 
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

316 
val atp_irrelevant_consts = 
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

317 
[@{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

318 
@{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

319 
@{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

320 

69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

321 
val atp_monomorph_bad_consts = 
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

322 
atp_irrelevant_consts @ 
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

323 
(* 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

324 
higherorder places) but not by the monomorphizer. *) 
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

325 
[@{const_name all}, @{const_name "==>"}, @{const_name "=="}, 
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

326 
@{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

327 
@{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

328 

43258
956895f99904
slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents:
43248
diff
changeset

329 
fun add_schematic_const (x as (_, T)) = 
956895f99904
slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents:
43248
diff
changeset

330 
Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x 
956895f99904
slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents:
43248
diff
changeset

331 
val add_schematic_consts_of = 
956895f99904
slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents:
43248
diff
changeset

332 
Term.fold_aterms (fn Const (x as (s, _)) => 
956895f99904
slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents:
43248
diff
changeset

333 
not (member (op =) atp_monomorph_bad_consts s) 
956895f99904
slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents:
43248
diff
changeset

334 
? add_schematic_const x 
956895f99904
slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents:
43248
diff
changeset

335 
 _ => I) 
956895f99904
slightly faster/cleaner accumulation of polymorphic consts
blanchet
parents:
43248
diff
changeset

336 
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

337 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

338 
(** 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

339 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

340 
(* The first component is the type class; the second is a "TVar" or "TFree". *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

341 
datatype type_literal = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

342 
TyLitVar of name * name  
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

343 
TyLitFree of name * name 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

344 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

345 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

346 
(** Isabelle arities **) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

347 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

348 
datatype arity_literal = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

349 
TConsLit of name * name * name list  
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

350 
TVarLit of name * name 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

351 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

352 
fun gen_TVars 0 = [] 
43093  353 
 gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n1) 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

354 

43263  355 
val type_class = the_single @{sort type} 
356 

357 
fun add_packed_sort tvar = 

358 
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

359 

43086  360 
type arity_clause = 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

361 
{name : string, 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

362 
prem_lits : arity_literal list, 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

363 
concl_lits : arity_literal} 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

364 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

365 
(* 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

366 
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

367 
let 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

368 
val tvars = gen_TVars (length args) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

369 
val tvars_srts = ListPair.zip (tvars, args) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

370 
in 
43086  371 
{name = name, 
43263  372 
prem_lits = [] > fold (uncurry add_packed_sort) tvars_srts > map TVarLit, 
43086  373 
concl_lits = TConsLit (`make_type_class cls, 
374 
`make_fixed_type_const tcons, 

375 
tvars ~~ tvars)} 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

376 
end 
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 
fun arity_clause _ _ (_, []) = [] 
43495  379 
 arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *) 
380 
arity_clause seen n (tcons, ars) 

381 
 arity_clause seen n (tcons, (ar as (class, _)) :: ars) = 

382 
if member (op =) seen class then 

383 
(* multiple arities for the same (tycon, class) pair *) 

384 
make_axiom_arity_clause (tcons, 

385 
lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n, 

386 
ar) :: 

387 
arity_clause seen (n + 1) (tcons, ars) 

388 
else 

389 
make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^ 

390 
ascii_of class, ar) :: 

391 
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

392 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

393 
fun multi_arity_clause [] = [] 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

394 
 multi_arity_clause ((tcons, ars) :: tc_arlists) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

395 
arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

396 

43622  397 
(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in 
398 
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

399 
fun type_class_pairs thy tycons classes = 
43093  400 
let 
401 
val alg = Sign.classes_of thy 

402 
fun domain_sorts tycon = Sorts.mg_domain alg tycon o single 

403 
fun add_class tycon class = 

404 
cons (class, domain_sorts tycon class) 

405 
handle Sorts.CLASS_ERROR _ => I 

406 
fun try_classes tycon = (tycon, fold (add_class tycon) classes []) 

407 
in map try_classes tycons end 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

408 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

409 
(*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

410 
fun iter_type_class_pairs _ _ [] = ([], []) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

411 
 iter_type_class_pairs thy tycons classes = 
43263  412 
let 
413 
fun maybe_insert_class s = 

414 
(s <> type_class andalso not (member (op =) classes s)) 

415 
? insert (op =) s 

416 
val cpairs = type_class_pairs thy tycons classes 

417 
val newclasses = 

418 
[] > fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs 

419 
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses 

43266  420 
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

421 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

422 
fun make_arity_clauses thy tycons = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

423 
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

424 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

425 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

426 
(** Isabelle class relations **) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

427 

43086  428 
type class_rel_clause = 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

429 
{name : string, 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

430 
subclass : name, 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

431 
superclass : name} 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

432 

43622  433 
(* Generate all pairs (sub, super) such that sub is a proper subclass of super 
434 
in theory "thy". *) 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

435 
fun class_pairs _ [] _ = [] 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

436 
 class_pairs thy subs supers = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

437 
let 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

438 
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

439 
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

440 
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

441 
in fold add_supers subs [] end 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

442 

43622  443 
fun make_class_rel_clause (sub, super) = 
444 
{name = sub ^ "_" ^ super, subclass = `make_type_class sub, 

43086  445 
superclass = `make_type_class super} 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

446 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

447 
fun make_class_rel_clauses thy subs supers = 
43093  448 
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

449 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

450 
datatype combterm = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

451 
CombConst of name * typ * typ list  
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

452 
CombVar of name * typ  
43677  453 
CombApp of combterm * combterm  
454 
CombAbs of (name * typ) * combterm 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

455 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

456 
fun combtyp_of (CombConst (_, T, _)) = T 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

457 
 combtyp_of (CombVar (_, T)) = T 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

458 
 combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1)) 
43677  459 
 combtyp_of (CombAbs ((_, T), tm)) = T > combtyp_of tm 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

460 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

461 
(*gets the head of a combinator application, along with the list of arguments*) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

462 
fun strip_combterm_comb u = 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

463 
let 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

464 
fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts) 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

465 
 stripc x = x 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

466 
in stripc (u, []) end 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

467 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

468 
fun atyps_of T = fold_atyps (insert (op =)) T [] 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

469 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

470 
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

471 
[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

472 
> space_implode Long_Name.separator 
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 
(* Converts a term (with combinators) into a combterm. Also accumulates sort 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

475 
infomation. *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

476 
fun combterm_from_term thy bs (P $ Q) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

477 
let 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

478 
val (P', P_atomics_Ts) = combterm_from_term thy bs P 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

479 
val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

480 
in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

481 
 combterm_from_term thy _ (Const (c, T)) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

482 
let 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

483 
val tvar_list = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

484 
(if String.isPrefix old_skolem_const_prefix c then 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

485 
[] > Term.add_tvarsT T > map TVar 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

486 
else 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

487 
(c, T) > Sign.const_typargs thy) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

488 
val c' = CombConst (`make_fixed_const c, T, tvar_list) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

489 
in (c', atyps_of T) end 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

490 
 combterm_from_term _ _ (Free (v, T)) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

491 
(CombConst (`make_fixed_var v, T, []), atyps_of T) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

492 
 combterm_from_term _ _ (Var (v as (s, _), T)) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

493 
(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

494 
let 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

495 
val Ts = T > strip_type > swap > op :: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

496 
val s' = new_skolem_const_name s (length Ts) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

497 
in CombConst (`make_fixed_const s', T, Ts) end 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

498 
else 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

499 
CombVar ((make_schematic_var v, s), T), atyps_of T) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

500 
 combterm_from_term _ bs (Bound j) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

501 
nth bs j 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

502 
> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T)) 
43677  503 
 combterm_from_term thy bs (Abs (s, T, t)) = 
43678  504 
let 
505 
fun vary s = s > AList.defined (op =) bs s ? vary o Symbol.bump_string 

506 
val s = vary s 

507 
val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t 

508 
in 

43677  509 
(CombAbs ((`make_bound_var s, T), tm), 
510 
union (op =) atomic_Ts (atyps_of T)) 

511 
end 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

512 

43421  513 
datatype locality = 
514 
General  Helper  Extensionality  Intro  Elim  Simp  Local  Assum  

515 
Chained 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

516 

0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

517 
(* (quasi)underapproximation of the truth *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

518 
fun is_locality_global Local = false 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

519 
 is_locality_global Assum = false 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

520 
 is_locality_global Chained = false 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

521 
 is_locality_global _ = true 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

522 

43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

523 
datatype order = First_Order  Higher_Order 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

524 
datatype polymorphism = Polymorphic  Monomorphic  Mangled_Monomorphic 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

525 
datatype type_level = 
43362  526 
All_Types  Noninf_Nonmono_Types  Fin_Nonmono_Types  Const_Arg_Types  
527 
No_Types 

43128  528 
datatype type_heaviness = Heavyweight  Lightweight 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

529 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

530 
datatype type_enc = 
43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

531 
Simple_Types of order * type_level  
42837  532 
Preds of polymorphism * type_level * type_heaviness  
533 
Tags of polymorphism * type_level * type_heaviness 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

534 

42689
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

535 
fun try_unsuffixes ss s = 
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

536 
fold (fn s' => fn NONE => try (unsuffix s') s  some => some) ss NONE 
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

537 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

538 
fun type_enc_from_string s = 
42722  539 
(case try (unprefix "poly_") s of 
540 
SOME s => (SOME Polymorphic, s) 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

541 
 NONE => 
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

542 
case try (unprefix "mono_") s of 
42722  543 
SOME s => (SOME Monomorphic, s) 
544 
 NONE => 

545 
case try (unprefix "mangled_") s of 

546 
SOME s => (SOME Mangled_Monomorphic, s) 

547 
 NONE => (NONE, s)) 

42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

548 
> (fn s => 
43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

549 
(* "_query" and "_bang" are for the ASCIIchallenged Metis and 
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

550 
Mirabelle. *) 
42689
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

551 
case try_unsuffixes ["?", "_query"] s of 
43362  552 
SOME s => (Noninf_Nonmono_Types, s) 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

553 
 NONE => 
42689
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

554 
case try_unsuffixes ["!", "_bang"] s of 
43362  555 
SOME s => (Fin_Nonmono_Types, s) 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

556 
 NONE => (All_Types, s)) 
42828  557 
> apsnd (fn s => 
42837  558 
case try (unsuffix "_heavy") s of 
43128  559 
SOME s => (Heavyweight, s) 
560 
 NONE => (Lightweight, s)) 

42837  561 
> (fn (poly, (level, (heaviness, core))) => 
562 
case (core, (poly, level, heaviness)) of 

43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

563 
("simple", (NONE, _, Lightweight)) => 
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

564 
Simple_Types (First_Order, level) 
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

565 
 ("simple_higher", (NONE, _, Lightweight)) => 
43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

566 
if level = Noninf_Nonmono_Types then raise Same.SAME 
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

567 
else Simple_Types (Higher_Order, level) 
42854
d99167ac4f8a
since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents:
42852
diff
changeset

568 
 ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) 
42886
208ec29cc013
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents:
42885
diff
changeset

569 
 ("tags", (SOME Polymorphic, _, _)) => 
43361
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

570 
Tags (Polymorphic, level, heaviness) 
42854
d99167ac4f8a
since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents:
42852
diff
changeset

571 
 ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) 
43128  572 
 ("args", (SOME poly, All_Types (* naja *), Lightweight)) => 
573 
Preds (poly, Const_Arg_Types, Lightweight) 

574 
 ("erased", (NONE, All_Types (* naja *), Lightweight)) => 

575 
Preds (Polymorphic, No_Types, Lightweight) 

42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

576 
 _ => raise Same.SAME) 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

577 
handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

578 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

579 
fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

580 
 is_type_enc_higher_order _ = false 
43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

581 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

582 
fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

583 
 polymorphism_of_type_enc (Preds (poly, _, _)) = poly 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

584 
 polymorphism_of_type_enc (Tags (poly, _, _)) = poly 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

585 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

586 
fun level_of_type_enc (Simple_Types (_, level)) = level 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

587 
 level_of_type_enc (Preds (_, level, _)) = level 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

588 
 level_of_type_enc (Tags (_, level, _)) = level 
42828  589 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

590 
fun heaviness_of_type_enc (Simple_Types _) = Heavyweight 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

591 
 heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

592 
 heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness 
42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

593 

42687  594 
fun is_type_level_virtually_sound level = 
43362  595 
level = All_Types orelse level = Noninf_Nonmono_Types 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

596 
val is_type_enc_virtually_sound = 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

597 
is_type_level_virtually_sound o level_of_type_enc 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

598 

23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

599 
fun is_type_level_fairly_sound level = 
43362  600 
is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

601 
val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

602 

43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

603 
fun choose_format formats (Simple_Types (order, level)) = 
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

604 
if member (op =) formats THF then 
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

605 
(THF, Simple_Types (order, level)) 
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

606 
else if member (op =) formats TFF then 
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

607 
(TFF, Simple_Types (First_Order, level)) 
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

608 
else 
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

609 
choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight)) 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

610 
 choose_format formats type_enc = 
43101
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

611 
(case hd formats of 
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

612 
CNF_UEQ => 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

613 
(CNF_UEQ, case type_enc of 
43101
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

614 
Preds stuff => 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

615 
(if is_type_enc_fairly_sound type_enc then Tags else Preds) 
43101
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

616 
stuff 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

617 
 _ => type_enc) 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

618 
 format => (format, type_enc)) 
43101
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

619 

40114  620 
type translated_formula = 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

621 
{name : string, 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

622 
locality : locality, 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

623 
kind : formula_kind, 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

624 
combformula : (name, typ, combterm) formula, 
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

625 
atomic_types : typ list} 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

626 

42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

627 
fun update_combformula f ({name, locality, kind, combformula, atomic_types} 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

628 
: translated_formula) = 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

629 
{name = name, locality = locality, kind = kind, combformula = f combformula, 
42562  630 
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

631 

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

632 
fun fact_lift f ({combformula, ...} : translated_formula) = f combformula 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

633 

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

634 
val type_instance = Sign.typ_instance o Proof_Context.theory_of 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

635 

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

636 
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

637 
let val T = get_T x in 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

638 
if exists (curry (type_instance ctxt) T o get_T) xs then xs 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

639 
else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

640 
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

641 

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

642 
(* 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

643 
datatype type_arg_policy = 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

644 
Explicit_Type_Args of bool  
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

645 
Mangled_Type_Args of bool  
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

646 
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

647 

42836  648 
fun should_drop_arg_type_args (Simple_Types _) = 
649 
false (* since TFF doesn't support overloading *) 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

650 
 should_drop_arg_type_args type_enc = 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

651 
level_of_type_enc type_enc = All_Types andalso 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

652 
heaviness_of_type_enc type_enc = Heavyweight 
42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

653 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

654 
fun type_arg_policy type_enc s = 
43628
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

655 
if s = type_tag_name then 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

656 
(if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then 
43623  657 
Mangled_Type_Args 
658 
else 

659 
Explicit_Type_Args) false 

43628
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

660 
else case type_enc of 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

661 
Tags (_, All_Types, Heavyweight) => No_Type_Args 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

662 
 _ => 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

663 
if level_of_type_enc type_enc = No_Types orelse 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

664 
s = @{const_name HOL.eq} orelse 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

665 
(s = app_op_name andalso 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

666 
level_of_type_enc type_enc = Const_Arg_Types) then 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

667 
No_Type_Args 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

668 
else 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

669 
should_drop_arg_type_args type_enc 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

670 
> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

671 
Mangled_Type_Args 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

672 
else 
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

673 
Explicit_Type_Args) 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

674 

43628
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

675 
(* Make literals for sorted type variables. *) 
43263  676 
fun generic_add_sorts_on_type (_, []) = I 
677 
 generic_add_sorts_on_type ((x, i), s :: ss) = 

678 
generic_add_sorts_on_type ((x, i), ss) 

679 
#> (if s = the_single @{sort HOL.type} then 

43093  680 
I 
681 
else if i = ~1 then 

43263  682 
insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x)) 
43093  683 
else 
43263  684 
insert (op =) (TyLitVar (`make_type_class s, 
685 
(make_schematic_type_var (x, i), x)))) 

686 
fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S) 

687 
 add_sorts_on_tfree _ = I 

688 
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z 

689 
 add_sorts_on_tvar _ = I 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

690 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

691 
fun type_literals_for_types type_enc add_sorts_on_typ Ts = 
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

692 
[] > level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts 
41137
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

693 

42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

694 
fun mk_aconns c phis = 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

695 
let val (phis', phi') = split_last phis in 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

696 
fold_rev (mk_aconn c) phis' phi' 
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

697 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

698 
fun mk_ahorn [] phi = phi 
42534
46e690db16b8
fake type declarations for fulltype args and mangled type encodings, so that type assumptions can be discharged
blanchet
parents:
42533
diff
changeset

699 
 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

700 
fun mk_aquant _ [] phi = phi 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

701 
 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

702 
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

703 
 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

704 

42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

705 
fun close_universally atom_vars phi = 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

706 
let 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

707 
fun formula_vars bounds (AQuant (_, xs, phi)) = 
42526  708 
formula_vars (map fst xs @ bounds) phi 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

709 
 formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

710 
 formula_vars bounds (AAtom tm) = 
42526  711 
union (op =) (atom_vars tm [] 
712 
> filter_out (member (op =) bounds o fst)) 

42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

713 
in mk_aquant AForall (formula_vars [] phi []) phi end 
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

714 

42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

715 
fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

716 
 combterm_vars (CombConst _) = I 
42574  717 
 combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) 
43677  718 
 combterm_vars (CombAbs (_, tm)) = combterm_vars tm 
42674  719 
fun close_combformula_universally phi = close_universally combterm_vars phi 
42522
413b56894f82
close ATP formulas universally earlier, so that we can add type predicates
blanchet
parents:
42521
diff
changeset

720 

43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

721 
fun term_vars bounds (ATerm (name as (s, _), tms)) = 
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

722 
(is_tptp_variable s andalso not (member (op =) bounds name)) 
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

723 
? insert (op =) (name, NONE) #> fold (term_vars bounds) tms 
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

724 
 term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm 
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

725 
fun close_formula_universally phi = close_universally (term_vars []) phi 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

726 

42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

727 
val homo_infinite_type_name = @{type_name ind} (* any infinite type *) 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

728 
val homo_infinite_type = Type (homo_infinite_type_name, []) 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

729 

43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

730 
fun ho_term_from_typ format type_enc = 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

731 
let 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

732 
fun term (Type (s, Ts)) = 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

733 
ATerm (case (is_type_enc_higher_order type_enc, s) of 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

734 
(true, @{type_name bool}) => `I tptp_bool_type 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

735 
 (true, @{type_name fun}) => `I tptp_fun_type 
43178
b5862142d378
use "" type only in THF and TFF  might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
blanchet
parents:
43175
diff
changeset

736 
 _ => if s = homo_infinite_type_name andalso 
b5862142d378
use "" type only in THF and TFF  might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
blanchet
parents:
43175
diff
changeset

737 
(format = TFF orelse format = THF) then 
b5862142d378
use "" type only in THF and TFF  might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
blanchet
parents:
43175
diff
changeset

738 
`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

739 
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

740 
`make_fixed_type_const s, 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

741 
map term Ts) 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

742 
 term (TFree (s, _)) = ATerm (`make_fixed_type_var s, []) 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

743 
 term (TVar ((x as (s, _)), _)) = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

744 
ATerm ((make_schematic_type_var x, s), []) 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

745 
in term end 
42562  746 

43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

747 
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 firstorder)
nik
parents:
43628
diff
changeset

748 
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

749 

42562  750 
(* 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

751 
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

752 

42562  753 
fun generic_mangled_type_name f (ATerm (name, [])) = f name 
754 
 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

755 
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

756 
^ ")" 
43692  757 
 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

758 

42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

759 
val bool_atype = AType (`I tptp_bool_type) 
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

760 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

761 
fun make_simple_type s = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

762 
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

763 
s = tptp_individual_type then 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

764 
s 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

765 
else 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

766 
simple_type_prefix ^ ascii_of s 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

767 

43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

768 
fun ho_type_from_ho_term type_enc pred_sym ary = 
42963  769 
let 
770 
fun to_atype ty = 

771 
AType ((make_simple_type (generic_mangled_type_name fst ty), 

772 
generic_mangled_type_name snd ty)) 

773 
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

774 
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

775 
 to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary  1)) tys 
43692  776 
 to_fo _ _ = raise Fail "unexpected type abstraction" 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

777 
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 firstorder)
nik
parents:
43628
diff
changeset

778 
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 firstorder)
nik
parents:
43628
diff
changeset

779 
 to_ho _ = raise Fail "unexpected type abstraction" 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

780 
in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end 
42963  781 

43677  782 
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 firstorder)
nik
parents:
43628
diff
changeset

783 
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 firstorder)
nik
parents:
43628
diff
changeset

784 
o ho_term_from_typ format type_enc 
42963  785 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

786 
fun mangled_const_name format type_enc T_args (s, s') = 
42963  787 
let 
43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes firstorder)
nik
parents:
43628
diff
changeset

788 
val ty_args = T_args > map_filter (ho_term_for_type_arg format type_enc) 
42963  789 
fun type_suffix f g = 
790 
fold_rev (curry (op ^) o g o prefix mangled_type_sep 

791 
o generic_mangled_type_name f) ty_args "" 

792 
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

793 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

794 
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

795 
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

796 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

797 
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

798 
(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

799 
 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

800 
[] >> 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

801 
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

802 
(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

803 

024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

804 
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

805 
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

806 
> 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

807 
(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

808 
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

809 
> 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

810 

42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

811 
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

812 
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

813 
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

814 
(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

815 
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

816 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

817 
fun introduce_proxies type_enc = 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

818 
let 
43017
944b19ab6003
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents:
43001
diff
changeset

819 
fun intro top_level (CombApp (tm1, tm2)) = 
944b19ab6003
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents:
43001
diff
changeset

820 
CombApp (intro top_level tm1, intro false tm2) 
944b19ab6003
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents:
43001
diff
changeset

821 
 intro top_level (CombConst (name as (s, _), T, T_args)) = 
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42569
diff
changeset

822 
(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

823 
SOME proxy_base => 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

824 
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

825 
case (top_level, s) of 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

826 
(_, "c_False") => (`I tptp_false, []) 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

827 
 (_, "c_True") => (`I tptp_true, []) 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

828 
 (false, "c_Not") => (`I tptp_not, []) 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

829 
 (false, "c_conj") => (`I tptp_and, []) 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

830 
 (false, "c_disj") => (`I tptp_or, []) 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

831 
 (false, "c_implies") => (`I tptp_implies, []) 
43678  832 
 (false, "c_All") => (`I tptp_ho_forall, []) 
833 
 (false, "c_Ex") => (`I tptp_ho_exists, []) 

43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

834 
 (false, s) => 
43017
944b19ab6003
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents:
43001
diff
changeset

835 
if is_tptp_equal s then (`I tptp_equal, []) 
944b19ab6003
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents:
43001
diff
changeset

836 
else (proxy_base >> prefix const_prefix, T_args) 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

837 
 _ => (name, []) 
42569
5737947e4c77
make sure that fequal keeps its type arguments for mangled type systems
blanchet
parents:
42568
diff
changeset

838 
else 
42574  839 
(proxy_base >> prefix const_prefix, T_args) 
840 
 NONE => (name, T_args)) 

841 
> (fn (name, T_args) => CombConst (name, T, T_args)) 

43677  842 
 intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm) 
43017
944b19ab6003
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents:
43001
diff
changeset

843 
 intro _ tm = tm 
944b19ab6003
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents:
43001
diff
changeset

844 
in intro true end 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

845 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

846 
fun combformula_from_prop thy type_enc eq_as_iff = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

847 
let 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

848 
fun do_term bs t atomic_types = 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

849 
combterm_from_term thy bs (Envir.eta_contract t) 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

850 
>> (introduce_proxies type_enc #> AAtom) 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

851 
> union (op =) atomic_types 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

852 
fun do_quant bs q s T t' = 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43304
diff
changeset

853 
let val s = singleton (Name.variant_list (map fst bs)) s in 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

854 
do_formula ((s, T) :: bs) t' 
42562  855 
#>> mk_aquant q [(`make_bound_var s, SOME T)] 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

856 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

857 
and do_conn bs c t1 t2 = 
43198  858 
do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

859 
and do_formula bs t = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

860 
case t of 
43096  861 
@{const Trueprop} $ t1 => do_formula bs t1 
862 
 @{const Not} $ t1 => do_formula bs t1 #>> mk_anot 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

863 
 Const (@{const_name All}, _) $ Abs (s, T, t') => 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

864 
do_quant bs AForall s T t' 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

865 
 Const (@{const_name Ex}, _) $ Abs (s, T, t') => 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

866 
do_quant bs AExists s T t' 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

867 
 @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

868 
 @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

869 
 @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

870 
 Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

871 
if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

872 
 _ => do_term bs t 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

873 
in do_formula [] end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

874 

43264
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
43263
diff
changeset

875 
fun presimplify_term _ [] t = t 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
43263
diff
changeset

876 
 presimplify_term ctxt presimp_consts t = 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
43263
diff
changeset

877 
t > exists_Const (member (op =) presimp_consts o fst) t 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
43263
diff
changeset

878 
? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
43263
diff
changeset

879 
#> Meson.presimplify ctxt 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
43263
diff
changeset

880 
#> prop_of) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

881 

41491  882 
fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

883 
fun conceal_bounds Ts t = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

884 
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

885 
(0 upto length Ts  1 ~~ Ts), t) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

886 
fun reveal_bounds Ts = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

887 
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

888 
(0 upto length Ts  1 ~~ Ts)) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

889 

43265  890 
fun is_fun_equality (@{const_name HOL.eq}, 
891 
Type (_, [Type (@{type_name fun}, _), _])) = true 

892 
 is_fun_equality _ = false 

893 

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

894 
fun extensionalize_term ctxt t = 
43265  895 
if exists_Const is_fun_equality t then 
896 
let val thy = Proof_Context.theory_of ctxt in 

897 
t > cterm_of thy > Meson.extensionalize_conv ctxt 

898 
> prop_of > Logic.dest_equals > snd 

899 
end 

900 
else 

901 
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

902 

43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

903 
fun generic_translate_lambdas do_lambdas ctxt t = 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

904 
let 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

905 
fun aux Ts t = 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

906 
case t of 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

907 
@{const Not} $ t1 => @{const Not} $ aux Ts t1 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

908 
 (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

909 
t0 $ Abs (s, T, aux (T :: Ts) t') 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

910 
 (t0 as Const (@{const_name All}, _)) $ t1 => 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

911 
aux Ts (t0 $ eta_expand Ts t1 1) 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

912 
 (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

913 
t0 $ Abs (s, T, aux (T :: Ts) t') 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

914 
 (t0 as Const (@{const_name Ex}, _)) $ t1 => 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

915 
aux Ts (t0 $ eta_expand Ts t1 1) 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

916 
 (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

917 
 (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

918 
 (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

919 
 (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

920 
$ t1 $ t2 => 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

921 
t0 $ aux Ts t1 $ aux Ts t2 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

922 
 _ => 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

923 
if not (exists_subterm (fn Abs _ => true  _ => false) t) then t 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

924 
else t > Envir.eta_contract > do_lambdas ctxt Ts 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

925 
val (t, ctxt') = Variable.import_terms true [t] ctxt >> the_single 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

926 
in t > aux [] > singleton (Variable.export_terms ctxt' ctxt) end 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

927 

d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

928 
fun do_conceal_lambdas Ts (t1 $ t2) = 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

929 
do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

930 
 do_conceal_lambdas Ts (Abs (_, T, t)) = 
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

931 
(* slightly unsound because of hash collisions *) 
43827
62d64709af3b
added option to control which lambda translation to use (for experiments)
blanchet
parents:
43693
diff
changeset

932 
Free (concealed_lambda_prefix ^ string_of_int (hash_term t), 
62d64709af3b
added option to control which lambda translation to use (for experiments)
blanchet
parents:
43693
diff
changeset

933 
T > fastype_of1 (Ts, t)) 
43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

934 
 do_conceal_lambdas _ t = t 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

935 
val conceal_lambdas = generic_translate_lambdas (K do_conceal_lambdas) 
43827
62d64709af3b
added option to control which lambda translation to use (for experiments)
blanchet
parents:
43693
diff
changeset

936 

43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

937 
fun do_introduce_combinators ctxt Ts = 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

938 
let val thy = Proof_Context.theory_of ctxt in 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

939 
conceal_bounds Ts 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

940 
#> cterm_of thy 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

941 
#> Meson_Clausify.introduce_combinators_in_cterm 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

942 
#> prop_of #> Logic.dest_equals #> snd 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

943 
#> reveal_bounds Ts 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

944 
end 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

945 
val introduce_combinators = generic_translate_lambdas do_introduce_combinators 
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

946 

d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

947 
fun process_abstractions_in_term ctxt trans_lambdas kind t = 
42361  948 
let val thy = Proof_Context.theory_of ctxt in 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

949 
if Meson.is_fol_term thy t then 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

950 
t 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

951 
else 
43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

952 
t > singleton trans_lambdas 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

953 
handle THM _ => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

954 
(* A type variable of sort "{}" will make abstraction fail. *) 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

955 
if kind = Conjecture then HOLogic.false_const 
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

956 
else HOLogic.true_const 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

957 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

958 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

959 
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the 
42353
7797efa897a1
correctly handle TFrees that occur in (local) facts  Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
blanchet
parents:
42237
diff
changeset

960 
same in Sledgehammer to prevent the discovery of unreplayable proofs. *) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

961 
fun freeze_term t = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

962 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

963 
fun aux (t $ u) = aux t $ aux u 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

964 
 aux (Abs (s, T, t)) = Abs (s, T, aux t) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

965 
 aux (Var ((s, i), T)) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

966 
Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

967 
 aux t = t 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

968 
in t > exists_subterm is_Var t ? aux end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

969 

43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

970 
fun preprocess_prop ctxt trans_lambdas presimp_consts kind t = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

971 
let 
42361  972 
val thy = Proof_Context.theory_of ctxt 
38608
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

973 
val t = t > Envir.beta_eta_contract 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42943
diff
changeset

974 
> transform_elim_prop 
41211
1e2e16bc0077
no need to do a superduper atomization if Metis fails afterwards anyway
blanchet
parents:
41199
diff
changeset

975 
> Object_Logic.atomize_term thy 
42563  976 
val need_trueprop = (fastype_of t = @{typ bool}) 
43096  977 
in 
978 
t > need_trueprop ? HOLogic.mk_Trueprop 

979 
> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) [] 

980 
> extensionalize_term ctxt 

43264
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
43263
diff
changeset

981 
> presimplify_term ctxt presimp_consts 
43120
a9c2cdf4ae97
make sure "Trueprop" is removed before combinators are added  the code is fragile in that respect
blanchet
parents:
43105
diff
changeset

982 
> perhaps (try (HOLogic.dest_Trueprop)) 
43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

983 
> process_abstractions_in_term ctxt trans_lambdas kind 
43096  984 
end 
985 

986 
(* making fact and conjecture formulas *) 

43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

987 
fun make_formula thy type_enc eq_as_iff name loc kind t = 
43096  988 
let 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

989 
val (combformula, atomic_types) = 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

990 
combformula_from_prop thy type_enc eq_as_iff t [] 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

991 
in 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

992 
{name = name, locality = loc, kind = kind, combformula = combformula, 
42562  993 
atomic_types = atomic_types} 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

994 
end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

995 

43857  996 
fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc 
997 
presimp_consts ((name, loc), t) = 

43096  998 
let val thy = Proof_Context.theory_of ctxt in 
43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

999 
case t > preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

1000 
> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name 
43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

1001 
loc Axiom of 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43293
diff
changeset

1002 
formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} => 
43096  1003 
if s = tptp_true then NONE else SOME formula 
43295
30aaab778416
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
blanchet
parents:
43293
diff
changeset

1004 
 formula => SOME formula 
43096  1005 
end 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

1006 

43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

1007 
fun make_conjecture ctxt format prem_kind type_enc trans_lambdas preproc 
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

1008 
presimp_consts ts = 
43096  1009 
let 
1010 
val thy = Proof_Context.theory_of ctxt 

1011 
val last = length ts  1 

1012 
in 

42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1013 
map2 (fn j => fn t => 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1014 
let 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1015 
val (kind, maybe_negate) = 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1016 
if j = last then 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1017 
(Conjecture, I) 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1018 
else 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1019 
(prem_kind, 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1020 
if prem_kind = Conjecture then update_combformula mk_anot 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1021 
else I) 
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1022 
in 
43264
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
43263
diff
changeset

1023 
t > preproc ? 
43856
d636b053d4ff
move more lambdahandling logic to Sledgehammer, from ATP module, for formal dependency reasons
blanchet
parents:
43830
diff
changeset

1024 
(preprocess_prop ctxt trans_lambdas presimp_consts kind 
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

1025 
#> freeze_term) 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

1026 
> make_formula thy type_enc (format <> CNF) (string_of_int j) 
43624
de026aecab9b
cleaner handling of higherorder simple types, so that it's also possible to use firstorder simple types with LEOII and company
blanchet
parents:
43623
diff
changeset

1027 
Local kind 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

1028 
> maybe_negate 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

1029 
end) 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

1030 
(0 upto last) ts 
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

1031 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

1032 

42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1033 
(** Finite and infinite type inference **) 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1034 

42886
208ec29cc013
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents:
42885
diff
changeset

1035 
fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S) 
208ec29cc013
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents:
42885
diff
changeset

1036 
 deep_freeze_atyp T = T 
208ec29cc013
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents:
42885
diff
changeset

1037 
val deep_freeze_type = map_atyps deep_freeze_atyp 
208ec29cc013
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents:
42885
diff
changeset

1038 

42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1039 
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1040 
dangerous because their "exhaust" properties can easily lead to unsound ATP 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1041 
proofs. On the other hand, all HOL infinite types can be given the same 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1042 
models in firstorder logic (via LÃ¶wenheimSkolem). *) 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1043 

42886
208ec29cc013
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents:
42885
diff
changeset

1044 
fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T = 
208ec29cc013
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents:
42885
diff
changeset

1045 
exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts 
42836  1046 
 should_encode_type _ _ All_Types _ = true 
43572
ae612a423dad
added "sound" option to force Sledgehammer to be pedantically sound
blanchet
parents:
43501
diff
changeset

1047 
 should_encode_type ctxt _ Fin_Nonmono_Types T = 
ae612a423dad
added "sound" option to force Sledgehammer to be pedantically sound
blanchet
parents:
43501
diff
changeset

1048 
is_type_surely_finite ctxt false T 
42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1049 
 should_encode_type _ _ _ _ = false 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1050 

42837  1051 
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness)) 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

1052 
should_predicate_on_var T = 
43128  1053 
(heaviness = Heavyweight orelse should_predicate_on_var ()) andalso 
42878
85ac4c12a4b7
slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents:
42855
diff
changeset

1054 
should_encode_type ctxt nonmono_Ts level T 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

1055 
 should_predicate_on_type _ _ _ _ _ = false 
42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1056 

42836  1057 
fun is_var_or_bound_var (CombConst ((s, _), _, _)) = 
1058 
String.isPrefix bound_var_prefix s 

1059 
 is_var_or_bound_var (CombVar _) = true 

1060 
 is_var_or_bound_var _ = false 

1061 

43361
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1062 
datatype tag_site = 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1063 
Top_Level of bool option  
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1064 
Eq_Arg of bool option  
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1065 
Elsewhere 
42829
1558741f8a72
started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents:
42828
diff
changeset

1066 

43361
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1067 
fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1068 
 should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1069 
u T = 
42837  1070 
(case heaviness of 
43128  1071 
Heavyweight => should_encode_type ctxt nonmono_Ts level T 
1072 
 Lightweight => 

42836  1073 
case (site, is_var_or_bound_var u) of 
43361
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1074 
(Eq_Arg pos, true) => 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1075 
(* The first disjunct prevents a subtle soundness issue explained in 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1076 
Blanchette's Ph.D. thesis. See also 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1077 
"formula_lines_for_lightweight_tags_sym_decl". *) 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1078 
(pos <> SOME false andalso poly = Polymorphic andalso 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1079 
level <> All_Types andalso heaviness = Lightweight andalso 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1080 
exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1081 
should_encode_type ctxt nonmono_Ts level T 
42829
1558741f8a72
started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents:
42828
diff
changeset

1082 
 _ => false) 
1558741f8a72
started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents:
42828
diff
changeset

1083 
 should_tag_with_type _ _ _ _ _ _ = false 
42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1084 

42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1085 
fun homogenized_type ctxt nonmono_Ts level = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1086 
let 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1087 
val should_encode = should_encode_type ctxt nonmono_Ts level 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1088 
fun homo 0 T = if should_encode T then T else homo_infinite_type 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1089 
 homo ary (Type (@{type_name fun}, [T1, T2])) = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1090 
homo 0 T1 > homo (ary  1) T2 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1091 
 homo _ _ = raise Fail "expected function type" 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1092 
in homo end 
42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1093 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

1094 
(** "hBOOL" and "hAPP" **) 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

1095 

42574  1096 
type sym_info = 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1097 
{pred_sym : bool, min_ary : int, max_ary : int, types : typ list} 
42563  1098 

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

1099 
fun add_combterm_syms_to_table ctxt explicit_apply = 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

1100 
let 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1101 
fun consider_var_arity const_T var_T max_ary = 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1102 
let 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1103 
fun iter ary T = 
43210
7384b771805d
made "explicit_apply"'s smart mode (more) complete
blanchet
parents:
43207
diff
changeset

1104 
if ary = max_ary orelse type_instance ctxt (var_T, T) orelse 
7384b771805d
made "explicit_apply"'s smart mode (more) complete
blanchet
parents:
43207
diff
changeset

1105 
type_instance ctxt (T, var_T) then 
7384b771805d
made "explicit_apply"'s smart mode (more) complete
blanchet
parents:
43207
diff
changeset

1106 
ary 
7384b771805d
made "explicit_apply"'s smart mode (more) complete
blanchet
parents:
43207
diff
changeset

1107 
else 
7384b771805d
made "explicit_apply"'s smart mode (more) complete
blanchet
parents:
43207
diff
changeset

1108 
iter (ary + 1) (range_type T) 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1109 
in iter 0 const_T end 
43201
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1110 
fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) = 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1111 
if explicit_apply = NONE andalso 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1112 
(can dest_funT T orelse T = @{typ bool}) then 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1113 
let 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1114 
val bool_vars' = bool_vars orelse body_type T = @{typ bool} 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1115 
fun repair_min_arity {pred_sym, min_ary, max_ary, types} = 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1116 
{pred_sym = pred_sym andalso not bool_vars', 
43213
e1fdd27e0c98
generate less type information in polymorphic case
blanchet
parents:
43210
diff
changeset

1117 
min_ary = fold (fn T' => consider_var_arity T' T) types min_ary, 
43201
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1118 
max_ary = max_ary, types = types} 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1119 
val fun_var_Ts' = 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1120 
fun_var_Ts > can dest_funT T ? insert_type ctxt I T 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1121 
in 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1122 
if bool_vars' = bool_vars andalso 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1123 
pointer_eq (fun_var_Ts', fun_var_Ts) then 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1124 
accum 
43167
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1125 
else 
43213
e1fdd27e0c98
generate less type information in polymorphic case
blanchet
parents:
43210
diff
changeset

1126 
((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab) 
43201
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1127 
end 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1128 
else 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1129 
accum 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1130 
fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) = 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1131 
let val (head, args) = strip_combterm_comb tm in 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

1132 
(case head of 
42563  1133 
CombConst ((s, _), T, _) => 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

1134 
if String.isPrefix bound_var_prefix s then 
43201
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1135 
add_var_or_bound_var T accum 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

1136 
else 
43139
9ed5d8ad8fa0
fixed debilitating translation bug introduced in b6e61d22fa61  "equal" and "=" should always have arity 2
blanchet
parents:
43136
diff
changeset

1137 
let val ary = length args in 
43201
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1138 
((bool_vars, fun_var_Ts), 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1139 
case Symtab.lookup sym_tab s of 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1140 
SOME {pred_sym, min_ary, max_ary, types} => 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1141 
let 
43201
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1142 
val pred_sym = 
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1143 
pred_sym andalso top_level andalso not bool_vars 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1144 
val types' = types > insert_type ctxt I T 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1145 
val min_ary = 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1146 
if is_some explicit_apply orelse 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1147 
pointer_eq (types', types) then 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1148 
min_ary 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1149 
else 
43201
0c9bf1a8e0d8
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higherorder quantification, namely "bool"s
blanchet
parents:
43198
diff
changeset

1150 
fold (consider_var_arity T) fun_var_Ts min_ary 