author  nik 
Tue, 30 Aug 2011 14:12:55 +0200  
changeset 44586  eeba1eedf32d 
parent 44585  cfe7f4a68e51 
child 44587  0f50f158eb57 
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 

43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

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

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

8 

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

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

10 
sig 
43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes 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 = 
44585  19 
General  Helper  Induction  Extensionality  Intro  Elim  Simp  
20 
Local  Assum  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 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44493
diff
changeset

23 
datatype polymorphism = Polymorphic  Raw_Monomorphic  Mangled_Monomorphic 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

24 
datatype soundness = Unsound  Sound_Modulo_Infiniteness  Sound 
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

25 
datatype type_level = 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

26 
All_Types  
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

27 
Noninf_Nonmono_Types of soundness  
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

28 
Fin_Nonmono_Types  
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

29 
Const_Arg_Types  
43362  30 
No_Types 
44402  31 
datatype type_uniformity = Uniform  Nonuniform 
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

32 

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

33 
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

34 
Simple_Types of order * type_level  
44402  35 
Guards of polymorphism * type_level * type_uniformity  
36 
Tags of polymorphism * type_level * type_uniformity 

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

37 

44496
c1884789ff80
added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents:
44495
diff
changeset

38 
val type_tag_idempotence : bool Config.T 
c1884789ff80
added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents:
44495
diff
changeset

39 
val type_tag_arguments : bool Config.T 
44088
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

40 
val no_lambdasN : string 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

41 
val concealedN : string 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

42 
val liftingN : string 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

43 
val combinatorsN : string 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

44 
val hybridN : string 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

45 
val lambdasN : string 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

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

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

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

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

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

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

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

53 
val class_prefix : string 
43936
127749bbc639
use a more robust naming convention for "polymorphic" frees  the check is an overapproximation but that's fine as far as soundness is concerned
blanchet
parents:
43907
diff
changeset

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

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

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

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

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

59 
val sym_decl_prefix : string 
43989  60 
val guards_sym_formula_prefix : string 
44396
66b9b3fcd608
started cleaning up polymorphic monotonicitybased encodings, based on discussions with Nick Smallbone
blanchet
parents:
44394
diff
changeset

61 
val 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

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

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

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

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

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

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

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

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

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

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

72 
val app_op_name : string 
44396
66b9b3fcd608
started cleaning up polymorphic monotonicitybased encodings, based on discussions with Nick Smallbone
blanchet
parents:
44394
diff
changeset

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

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

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

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

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

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

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

81 
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

82 
val proxy_table : (string * (string * (thm * (string * string)))) list 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

83 
val proxify_const : string > (string * string) option 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

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

85 
val unproxify_const : string > string 
43093  86 
val new_skolem_var_name_from_const : string > string 
43248
69375eaa9016
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
blanchet
parents:
43222
diff
changeset

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

88 
val atp_schematic_consts_of : term > typ list Symtab.table 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

89 
val type_enc_from_string : soundness > 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

90 
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

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

92 
val level_of_type_enc : type_enc > type_level 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

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

94 
val is_type_enc_fairly_sound : type_enc > bool 
44416
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44410
diff
changeset

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

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

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

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

99 
val unmangled_const_name : string > string 
43194  100 
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

101 
val factsN : string 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39975
diff
changeset

102 
val prepare_atp_problem : 
44394
20bd9f90accc
added option to control soundness of encodings more precisely, for evaluation purposes
blanchet
parents:
44393
diff
changeset

103 
Proof.context > format > formula_kind > formula_kind > type_enc 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

104 
> bool > string > bool > bool > term list > term 
44088
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

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

106 
> string problem * string Symtab.table * int * int 
43214  107 
* (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

108 
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

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

110 

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

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

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

113 

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

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

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

116 

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

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

118 

44496
c1884789ff80
added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents:
44495
diff
changeset

119 
val type_tag_idempotence = 
44540
968115499161
change default for generation of tag idempotence and tag argument equations
blanchet
parents:
44508
diff
changeset

120 
Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false) 
44496
c1884789ff80
added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents:
44495
diff
changeset

121 
val type_tag_arguments = 
44540
968115499161
change default for generation of tag idempotence and tag argument equations
blanchet
parents:
44508
diff
changeset

122 
Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false) 
44496
c1884789ff80
added config options to control two aspects of the translation, for evaluation purposes
blanchet
parents:
44495
diff
changeset

123 

44088
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

124 
val no_lambdasN = "no_lambdas" 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

125 
val concealedN = "concealed" 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

126 
val liftingN = "lifting" 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

127 
val combinatorsN = "combinators" 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

128 
val hybridN = "hybrid" 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

129 
val lambdasN = "lambdas" 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

130 
val smartN = "smart" 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

131 

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

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

133 

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

136 
else NONE 

42879  137 

43693  138 
val introN = "intro" 
139 
val elimN = "elim" 

140 
val simpN = "simp" 

42879  141 

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

142 
val bound_var_prefix = "B_" 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

143 
val all_bound_var_prefix = "BA_" 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

144 
val exist_bound_var_prefix = "BE_" 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

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

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

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

150 
val type_const_prefix = "tc_" 
44491
ba22ed224b20
fixed bang encoding detection of which types to encode
blanchet
parents:
44463
diff
changeset

151 
val simple_type_prefix = "s_" 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

153 

43936
127749bbc639
use a more robust naming convention for "polymorphic" frees  the check is an overapproximation but that's fine as far as soundness is concerned
blanchet
parents:
43907
diff
changeset

154 
val polymorphic_free_prefix = "poly_free" 
43907
073ab5379842
pass type arguments to lambdalifted Frees, to account for polymorphism
blanchet
parents:
43906
diff
changeset

155 

43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

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

157 
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

158 
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

159 

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

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

161 
val sym_decl_prefix = "sy_" 
43989  162 
val guards_sym_formula_prefix = "gsy_" 
44396
66b9b3fcd608
started cleaning up polymorphic monotonicitybased encodings, based on discussions with Nick Smallbone
blanchet
parents:
44394
diff
changeset

163 
val 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

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

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

166 
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

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

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

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

170 

43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

171 
val lambda_fact_prefix = "ATP.lambda_" 
42881
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

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

173 
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

174 
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

175 

44491
ba22ed224b20
fixed bang encoding detection of which types to encode
blanchet
parents:
44463
diff
changeset

176 
val predicator_name = "pp" 
ba22ed224b20
fixed bang encoding detection of which types to encode
blanchet
parents:
44463
diff
changeset

177 
val app_op_name = "aa" 
ba22ed224b20
fixed bang encoding detection of which types to encode
blanchet
parents:
44463
diff
changeset

178 
val type_guard_name = "gg" 
ba22ed224b20
fixed bang encoding detection of which types to encode
blanchet
parents:
44463
diff
changeset

179 
val type_tag_name = "tt" 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

180 

43174  181 
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

182 
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

183 
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

184 

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

185 
(* Freshness almost guaranteed! *) 
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

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

187 

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

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

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

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

191 
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

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

194 

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

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

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

197 
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

198 

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

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

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

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

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

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

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

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

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

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

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

209 

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

210 
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

211 

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

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

213 

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

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

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

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

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

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

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

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

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

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

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

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

225 
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

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

227 
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

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

229 
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

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

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

232 
 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

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

234 

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

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

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

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

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

239 
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

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

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

242 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

256 
("equal", (@{const_name HOL.eq}, (@{thm fequal_def}, 
43678  257 
("fequal", @{const_name ATP.fequal})))), 
258 
("c_All", (@{const_name All}, (@{thm fAll_def}, 

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

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

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

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

262 

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

263 
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

264 

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

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

266 
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

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

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

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

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

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

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

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

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

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

276 
(@{const_name HOL.eq}, "equal"), 
43678  277 
(@{const_name All}, "All"), 
278 
(@{const_name Ex}, "Ex"), 

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

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

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

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

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

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

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

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

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

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

288 

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

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

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

291 
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

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

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

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

295 

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

296 
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

297 
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

298 

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

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

300 
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

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

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

303 

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

306 

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

307 
fun make_bound_var x = bound_var_prefix ^ ascii_of x 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

308 
fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

309 
fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

310 
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

311 
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

312 

43622  313 
fun make_schematic_type_var (x, i) = 
314 
tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) 

315 
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

316 

43622  317 
(* "HOL.eq" is mapped to the ATP's equality. *) 
44495  318 
fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal 
319 
 make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) = 

320 
tptp_choice 

321 
 make_fixed_const _ c = const_prefix ^ lookup_const c 

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

322 

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

323 
fun make_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

324 

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

325 
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

326 

43093  327 
fun new_skolem_var_name_from_const s = 
328 
let val ss = s > space_explode Long_Name.separator in 

329 
nth ss (length ss  2) 

330 
end 

331 

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

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

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

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

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

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

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

338 

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

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

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

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

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

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

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

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

346 

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

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

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

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

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

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

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

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

354 
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

355 

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

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

357 

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

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

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

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

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

362 

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

363 

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

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

365 

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

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

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

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

369 

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

370 
fun gen_TVars 0 = [] 
43093  371 
 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

372 

43263  373 
val type_class = the_single @{sort type} 
374 

375 
fun add_packed_sort tvar = 

376 
fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar)) 

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

377 

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

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

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

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

382 

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

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

384 
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

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

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

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

388 
in 
43086  389 
{name = name, 
43263  390 
prem_lits = [] > fold (uncurry add_packed_sort) tvars_srts > map TVarLit, 
43086  391 
concl_lits = TConsLit (`make_type_class cls, 
392 
`make_fixed_type_const tcons, 

393 
tvars ~~ tvars)} 

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

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

395 

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

396 
fun arity_clause _ _ (_, []) = [] 
43495  397 
 arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *) 
398 
arity_clause seen n (tcons, ars) 

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

400 
if member (op =) seen class then 

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

402 
make_axiom_arity_clause (tcons, 

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

404 
ar) :: 

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

406 
else 

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

408 
ascii_of class, ar) :: 

409 
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

410 

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

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

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

413 
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

414 

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

417 
fun type_class_pairs thy tycons classes = 
43093  418 
let 
419 
val alg = Sign.classes_of thy 

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

421 
fun add_class tycon class = 

422 
cons (class, domain_sorts tycon class) 

423 
handle Sorts.CLASS_ERROR _ => I 

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

425 
in map try_classes tycons end 

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

426 

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

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

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

429 
 iter_type_class_pairs thy tycons classes = 
43263  430 
let 
431 
fun maybe_insert_class s = 

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

433 
? insert (op =) s 

434 
val cpairs = type_class_pairs thy tycons classes 

435 
val newclasses = 

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

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

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

439 

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

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

441 
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

442 

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

443 

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

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

445 

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

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

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

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

450 

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

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

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

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

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

456 
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

457 
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

458 
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

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

460 

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

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

464 

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

465 
fun make_class_rel_clauses thy subs supers = 
43093  466 
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

467 

43859  468 
(* intermediate terms *) 
469 
datatype iterm = 

470 
IConst of name * typ * typ list  

471 
IVar of name * typ  

472 
IApp of iterm * iterm  

473 
IAbs of (name * typ) * iterm 

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

474 

43859  475 
fun ityp_of (IConst (_, T, _)) = T 
476 
 ityp_of (IVar (_, T)) = T 

477 
 ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1)) 

478 
 ityp_of (IAbs ((_, T), tm)) = T > ityp_of tm 

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

479 

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

480 
(*gets the head of a combinator application, along with the list of arguments*) 
43859  481 
fun strip_iterm_comb u = 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

482 
let 
43859  483 
fun stripc (IApp (t, u), ts) = stripc (t, u :: ts) 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

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

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

486 

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

487 
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

488 

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

489 
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

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

491 
> space_implode Long_Name.separator 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

492 

43859  493 
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term. 
494 
Also accumulates sort infomation. *) 

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

496 
let 
44495  497 
val (P', P_atomics_Ts) = iterm_from_term thy format bs P 
498 
val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q 

43859  499 
in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end 
44495  500 
 iterm_from_term thy format _ (Const (c, T)) = 
501 
(IConst (`(make_fixed_const (SOME format)) c, T, 

43907
073ab5379842
pass type arguments to lambdalifted Frees, to account for polymorphism
blanchet
parents:
43906
diff
changeset

502 
if String.isPrefix old_skolem_const_prefix c then 
073ab5379842
pass type arguments to lambdalifted Frees, to account for polymorphism
blanchet
parents:
43906
diff
changeset

503 
[] > Term.add_tvarsT T > map TVar 
073ab5379842
pass type arguments to lambdalifted Frees, to account for polymorphism
blanchet
parents:
43906
diff
changeset

504 
else 
073ab5379842
pass type arguments to lambdalifted Frees, to account for polymorphism
blanchet
parents:
43906
diff
changeset

505 
(c, T) > Sign.const_typargs thy), 
073ab5379842
pass type arguments to lambdalifted Frees, to account for polymorphism
blanchet
parents:
43906
diff
changeset

506 
atyps_of T) 
44495  507 
 iterm_from_term _ _ _ (Free (s, T)) = 
43907
073ab5379842
pass type arguments to lambdalifted Frees, to account for polymorphism
blanchet
parents:
43906
diff
changeset

508 
(IConst (`make_fixed_var s, T, 
43936
127749bbc639
use a more robust naming convention for "polymorphic" frees  the check is an overapproximation but that's fine as far as soundness is concerned
blanchet
parents:
43907
diff
changeset

509 
if String.isPrefix polymorphic_free_prefix s then [T] else []), 
43907
073ab5379842
pass type arguments to lambdalifted Frees, to account for polymorphism
blanchet
parents:
43906
diff
changeset

510 
atyps_of T) 
44495  511 
 iterm_from_term _ format _ (Var (v as (s, _), T)) = 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

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

515 
val s' = new_skolem_const_name s (length Ts) 
44495  516 
in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

517 
else 
43859  518 
IVar ((make_schematic_var v, s), T), atyps_of T) 
44495  519 
 iterm_from_term _ _ bs (Bound j) = 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

520 
nth bs j > (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T)) 
44495  521 
 iterm_from_term thy format bs (Abs (s, T, t)) = 
43678  522 
let 
523 
fun vary s = s > AList.defined (op =) bs s ? vary o Symbol.bump_string 

524 
val s = vary s 

44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

525 
val name = `make_bound_var s 
44495  526 
val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

527 
in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

528 

43421  529 
datatype locality = 
44585  530 
General  Helper  Induction  Extensionality  Intro  Elim  Simp  
531 
Local  Assum  Chained 

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

532 

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

533 
datatype order = First_Order  Higher_Order 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44493
diff
changeset

534 
datatype polymorphism = Polymorphic  Raw_Monomorphic  Mangled_Monomorphic 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

535 
datatype soundness = Unsound  Sound_Modulo_Infiniteness  Sound 
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

536 
datatype type_level = 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

537 
All_Types  
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

538 
Noninf_Nonmono_Types of soundness  
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

539 
Fin_Nonmono_Types  
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

540 
Const_Arg_Types  
43362  541 
No_Types 
44402  542 
datatype type_uniformity = Uniform  Nonuniform 
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

543 

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

544 
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

545 
Simple_Types of order * type_level  
44402  546 
Guards of polymorphism * type_level * type_uniformity  
547 
Tags of polymorphism * type_level * type_uniformity 

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 

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

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

550 
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

551 

44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

552 
fun type_enc_from_string soundness s = 
42722  553 
(case try (unprefix "poly_") s of 
554 
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

555 
 NONE => 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44493
diff
changeset

556 
case try (unprefix "raw_mono_") s of 
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44493
diff
changeset

557 
SOME s => (SOME Raw_Monomorphic, s) 
42722  558 
 NONE => 
44494
a77901b3774e
rationalized option names  mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44493
diff
changeset

559 
case try (unprefix "mono_") s of 
42722  560 
SOME s => (SOME Mangled_Monomorphic, s) 
561 
 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

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

563 
(* "_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

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

565 
case try_unsuffixes ["?", "_query"] s of 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

566 
SOME s => (Noninf_Nonmono_Types soundness, 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

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

568 
case try_unsuffixes ["!", "_bang"] s of 
43362  569 
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

570 
 NONE => (All_Types, s)) 
42828  571 
> apsnd (fn s => 
44402  572 
case try (unsuffix "_uniform") s of 
573 
SOME s => (Uniform, s) 

574 
 NONE => (Nonuniform, s)) 

575 
> (fn (poly, (level, (uniformity, core))) => 

576 
case (core, (poly, level, uniformity)) of 

577 
("simple", (NONE, _, Nonuniform)) => 

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

578 
Simple_Types (First_Order, level) 
44402  579 
 ("simple_higher", (NONE, _, Nonuniform)) => 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

580 
(case level of 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

581 
Noninf_Nonmono_Types _ => raise Same.SAME 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

582 
 _ => Simple_Types (Higher_Order, level)) 
44402  583 
 ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity) 
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

584 
 ("tags", (SOME Polymorphic, _, _)) => 
44402  585 
Tags (Polymorphic, level, uniformity) 
586 
 ("tags", (SOME poly, _, _)) => Tags (poly, level, uniformity) 

587 
 ("args", (SOME poly, All_Types (* naja *), Nonuniform)) => 

588 
Guards (poly, Const_Arg_Types, Nonuniform) 

589 
 ("erased", (NONE, All_Types (* naja *), Nonuniform)) => 

590 
Guards (Polymorphic, No_Types, Nonuniform) 

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

591 
 _ => 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

592 
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

593 

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

594 
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

595 
 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

596 

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

597 
fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic 
43989  598 
 polymorphism_of_type_enc (Guards (poly, _, _)) = poly 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

599 
 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

600 

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

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

603 
 level_of_type_enc (Tags (_, level, _)) = level 
42828  604 

44402  605 
fun uniformity_of_type_enc (Simple_Types _) = Uniform 
606 
 uniformity_of_type_enc (Guards (_, _, uniformity)) = uniformity 

607 
 uniformity_of_type_enc (Tags (_, _, uniformity)) = uniformity 

42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

608 

44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

609 
fun is_type_level_quasi_sound All_Types = true 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

610 
 is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

611 
 is_type_level_quasi_sound _ = false 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

612 
val is_type_enc_quasi_sound = 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

613 
is_type_level_quasi_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

614 

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

615 
fun is_type_level_fairly_sound level = 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

616 
is_type_level_quasi_sound level orelse level = Fin_Nonmono_Types 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

617 
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

618 

44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

619 
fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

620 
 is_type_level_monotonicity_based Fin_Nonmono_Types = true 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

621 
 is_type_level_monotonicity_based _ = false 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

622 

44416
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44410
diff
changeset

623 
fun adjust_type_enc (THF _) type_enc = type_enc 
44499  624 
 adjust_type_enc (TFF _) (Simple_Types (_, level)) = 
44416
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44410
diff
changeset

625 
Simple_Types (First_Order, level) 
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44410
diff
changeset

626 
 adjust_type_enc format (Simple_Types (_, level)) = 
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44410
diff
changeset

627 
adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform)) 
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44410
diff
changeset

628 
 adjust_type_enc CNF_UEQ (type_enc as Guards stuff) = 
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44410
diff
changeset

629 
(if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff 
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44410
diff
changeset

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

631 

44088
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

632 
fun lift_lambdas ctxt type_enc = 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

633 
map (close_form o Envir.eta_contract) #> rpair ctxt 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

634 
#> Lambda_Lifting.lift_lambdas 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

635 
(if polymorphism_of_type_enc type_enc = Polymorphic then 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

636 
SOME polymorphic_free_prefix 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

637 
else 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

638 
NONE) 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

639 
Lambda_Lifting.is_quantifier 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

640 
#> fst 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

641 

3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

642 
fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) = 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

643 
intentionalize_def t 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

644 
 intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) = 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

645 
let 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

646 
fun lam T t = Abs (Name.uu, T, t) 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

647 
val (head, args) = strip_comb t > rev 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

648 
val head_T = fastype_of head 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

649 
val n = length args 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

650 
val arg_Ts = head_T > binder_types > take n > rev 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

651 
val u = u > subst_atomic (args ~~ map Bound (0 upto n  1)) 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

652 
in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

653 
 intentionalize_def t = t 
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

654 

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

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

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

658 
kind : formula_kind, 
43859  659 
iformula : (name, typ, iterm) formula, 
43496
92f5a4c78b37
remove historical bloat  another benefit of merging Metis's and Sledgehammer's translations
blanchet
parents:
43495
diff
changeset

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

661 

43859  662 
fun update_iformula f ({name, locality, kind, iformula, atomic_types} 
663 
: translated_formula) = 

664 
{name = name, locality = locality, kind = kind, iformula = f iformula, 

42562  665 
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

666 

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

668 

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

669 
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

670 
let val T = get_T x in 
44399  671 
if exists (type_instance ctxt T o get_T) xs then xs 
672 
else x :: filter_out (type_generalization ctxt T o get_T) xs 

43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

673 
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

674 

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

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

676 
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

677 
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

678 
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

679 
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

680 

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

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

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

684 
level_of_type_enc type_enc = All_Types andalso 
44402  685 
uniformity_of_type_enc type_enc = Uniform 
42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

686 

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

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

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

689 
(if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then 
43623  690 
Mangled_Type_Args 
691 
else 

692 
Explicit_Type_Args) false 

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

693 
else case type_enc of 
44402  694 
Tags (_, All_Types, Uniform) => No_Type_Args 
43628
996b2022ff78
further repair "mangled_tags", now that tags are also mangled
blanchet
parents:
43626
diff
changeset

695 
 _ => 
44398  696 
let val level = level_of_type_enc type_enc in 
697 
if level = No_Types orelse s = @{const_name HOL.eq} orelse 

698 
(s = app_op_name andalso level = Const_Arg_Types) then 

699 
No_Type_Args 

700 
else 

701 
should_drop_arg_type_args type_enc 

702 
> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then 

703 
Mangled_Type_Args 

704 
else 

705 
Explicit_Type_Args) 

706 
end 

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

707 

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

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

711 
generic_add_sorts_on_type ((x, i), ss) 

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

43093  713 
I 
714 
else if i = ~1 then 

43263  715 
insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x)) 
43093  716 
else 
43263  717 
insert (op =) (TyLitVar (`make_type_class s, 
718 
(make_schematic_type_var (x, i), x)))) 

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

720 
 add_sorts_on_tfree _ = I 

721 
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z 

722 
 add_sorts_on_tvar _ = I 

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

723 

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

724 
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

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

726 

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

727 
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

728 
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

729 
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

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

731 
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

732 
 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

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

734 
 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

735 
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

736 
 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

737 

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

738 
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

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

740 
fun formula_vars bounds (AQuant (_, xs, phi)) = 
42526  741 
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

742 
 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

743 
 formula_vars bounds (AAtom tm) = 
42526  744 
union (op =) (atom_vars tm [] 
745 
> 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

746 
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

747 

43859  748 
fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2] 
749 
 iterm_vars (IConst _) = I 

750 
 iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T) 

751 
 iterm_vars (IAbs (_, tm)) = iterm_vars tm 

752 
fun close_iformula_universally phi = close_universally iterm_vars phi 

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

753 

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

754 
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

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

756 
? 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

757 
 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

758 
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

759 

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

760 
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

761 
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

762 

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

763 
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

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

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

766 
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

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

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

769 
 _ => if s = homo_infinite_type_name andalso 
44235
85e9dad3c187
distinguish THF syntax with and without choice (Satallax vs. LEOII)
blanchet
parents:
44121
diff
changeset

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

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

772 
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

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

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

775 
 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

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

777 
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

778 
in term end 
42562  779 

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

780 
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

781 
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

782 

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

784 
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

785 

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

788 
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

789 
^ ")" 
43692  790 
 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

791 

44396
66b9b3fcd608
started cleaning up polymorphic monotonicitybased encodings, based on discussions with Nick Smallbone
blanchet
parents:
44394
diff
changeset

792 
fun mangled_type format type_enc = 
66b9b3fcd608
started cleaning up polymorphic monotonicitybased encodings, based on discussions with Nick Smallbone
blanchet
parents:
44394
diff
changeset

793 
generic_mangled_type_name fst o ho_term_from_typ format type_enc 
66b9b3fcd608
started cleaning up polymorphic monotonicitybased encodings, based on discussions with Nick Smallbone
blanchet
parents:
44394
diff
changeset

794 

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

795 
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

796 

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

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

798 
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

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

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

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

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

803 

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

804 
fun ho_type_from_ho_term type_enc pred_sym ary = 
42963  805 
let 
806 
fun to_atype ty = 

807 
AType ((make_simple_type (generic_mangled_type_name fst ty), 

808 
generic_mangled_type_name snd ty)) 

809 
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

810 
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

811 
 to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary  1)) tys 
43692  812 
 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

813 
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

814 
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

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

816 
in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end 
42963  817 

43677  818 
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

819 
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

820 
o ho_term_from_typ format type_enc 
42963  821 

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

822 
fun mangled_const_name format type_enc T_args (s, s') = 
42963  823 
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

824 
val ty_args = T_args > map_filter (ho_term_for_type_arg format type_enc) 
42963  825 
fun type_suffix f g = 
826 
fold_rev (curry (op ^) o g o prefix mangled_type_sep 

827 
o generic_mangled_type_name f) ty_args "" 

828 
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

829 

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

830 
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

831 
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

832 

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

833 
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

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

835 
 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

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

837 
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

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

839 

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

840 
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

841 
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

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

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

844 
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

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

846 

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

847 
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

848 
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

849 
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

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

851 
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

852 

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

853 
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

854 
let 
43987
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

855 
fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, []) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

856 
 tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

857 
_ = 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

858 
(* Etaexpand "!!" and "??", to work around LEOII 1.2.8 parser 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

859 
limitation. This works in conjuction with special code in 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

860 
"ATP_Problem" that uses the syntactic sugar "!" and "?" whenever 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

861 
possible. *) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

862 
IAbs ((`I "P", p_T), 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

863 
IApp (IConst (`I ho_quant, T, []), 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

864 
IAbs ((`I "X", x_T), 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

865 
IApp (IConst (`I "P", p_T, []), 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

866 
IConst (`I "X", x_T, []))))) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

867 
 tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier" 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

868 
fun intro top_level args (IApp (tm1, tm2)) = 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

869 
IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

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

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

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

873 
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

874 
case (top_level, s) of 
43987
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

875 
(_, "c_False") => IConst (`I tptp_false, T, []) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

876 
 (_, "c_True") => IConst (`I tptp_true, T, []) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

877 
 (false, "c_Not") => IConst (`I tptp_not, T, []) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

878 
 (false, "c_conj") => IConst (`I tptp_and, T, []) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

879 
 (false, "c_disj") => IConst (`I tptp_or, T, []) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

880 
 (false, "c_implies") => IConst (`I tptp_implies, T, []) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

881 
 (false, "c_All") => tweak_ho_quant tptp_ho_forall T args 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

882 
 (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

883 
 (false, s) => 
44097  884 
if is_tptp_equal s andalso length args = 2 then 
885 
IConst (`I tptp_equal, T, []) 

886 
else 

887 
(* Use a proxy even for partially applied THF equality, because 

888 
the LEOII and Satallax parsers complain about not being 

889 
able to infer the type of "=". *) 

890 
IConst (proxy_base >> prefix const_prefix, T, T_args) 

43987
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

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

892 
else 
43987
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

893 
IConst (proxy_base >> prefix const_prefix, T, T_args) 
44495  894 
 NONE => if s = tptp_choice then 
895 
tweak_ho_quant tptp_choice T args 

896 
else IConst (name, T, T_args)) 

43987
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

897 
 intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

898 
 intro _ _ tm = tm 
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

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

900 

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

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

903 
fun do_term bs t atomic_types = 
44495  904 
iterm_from_term thy format bs (Envir.eta_contract t) 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43624
diff
changeset

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

906 
> union (op =) atomic_types 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

907 
fun do_quant bs q pos s T t' = 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

908 
let 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

909 
val s = singleton (Name.variant_list (map fst bs)) s 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

910 
val universal = Option.map (q = AExists ? not) pos 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

911 
val name = 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

912 
s > `(case universal of 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

913 
SOME true => make_all_bound_var 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

914 
 SOME false => make_exist_bound_var 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

915 
 NONE => make_bound_var) 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

916 
in 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

917 
do_formula ((s, (name, T)) :: bs) pos t' 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

918 
#>> mk_aquant q [(name, SOME T)] 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

919 
end 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

920 
and do_conn bs c pos1 t1 pos2 t2 = 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

921 
do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c) 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

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

923 
case t of 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

924 
@{const Trueprop} $ t1 => do_formula bs pos t1 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

925 
 @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

926 
 Const (@{const_name All}, _) $ Abs (s, T, t') => 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

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

928 
 Const (@{const_name Ex}, _) $ Abs (s, T, t') => 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

929 
do_quant bs AExists pos s T t' 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

930 
 @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

931 
 @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

932 
 @{const HOL.implies} $ t1 $ t2 => 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

933 
do_conn bs AImplies (Option.map not pos) t1 pos t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

934 
 Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

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

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

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

938 

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

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

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

941 
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

942 
? (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

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

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

945 

43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

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

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

948 
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

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

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

951 
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

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

953 

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

956 
 is_fun_equality _ = false 

957 

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

958 
fun extensionalize_term ctxt t = 
43265  959 
if exists_Const is_fun_equality t then 
960 
let val thy = Proof_Context.theory_of ctxt in 

961 
t > cterm_of thy > Meson.extensionalize_conv ctxt 

962 
> prop_of > Logic.dest_equals > snd 

963 
end 

964 
else 

965 
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

966 

43862  967 
fun simple_translate_lambdas do_lambdas ctxt t = 
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

968 
let val thy = Proof_Context.theory_of ctxt in 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

969 
if Meson.is_fol_term thy t then 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

970 
t 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

971 
else 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

972 
let 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

973 
fun aux Ts t = 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

974 
case t of 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

975 
@{const Not} $ t1 => @{const Not} $ aux Ts t1 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

976 
 (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

977 
t0 $ Abs (s, T, aux (T :: Ts) t') 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

978 
 (t0 as Const (@{const_name All}, _)) $ t1 => 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

979 
aux Ts (t0 $ eta_expand Ts t1 1) 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

980 
 (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

981 
t0 $ Abs (s, T, aux (T :: Ts) t') 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

982 
 (t0 as Const (@{const_name Ex}, _)) $ t1 => 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

983 
aux Ts (t0 $ eta_expand Ts t1 1) 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

984 
 (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

985 
 (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

986 
 (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

987 
 (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

988 
$ t1 $ t2 => 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

989 
t0 $ aux Ts t1 $ aux Ts t2 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

990 
 _ => 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

991 
if not (exists_subterm (fn Abs _ => true  _ => false) t) then t 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

992 
else t > Envir.eta_contract > do_lambdas ctxt Ts 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

993 
val (t, ctxt') = Variable.import_terms true [t] ctxt >> the_single 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

994 
in t > aux [] > singleton (Variable.export_terms ctxt' ctxt) end 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

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

996 

43997  997 
fun do_cheaply_conceal_lambdas Ts (t1 $ t2) = 
998 
do_cheaply_conceal_lambdas Ts t1 

999 
$ do_cheaply_conceal_lambdas Ts t2 

1000 
 do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) = 

1001 
Free (polymorphic_free_prefix ^ serial_string (), 

1002 
T > fastype_of1 (T :: Ts, t)) 

1003 
 do_cheaply_conceal_lambdas _ t = t 

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

1004 

43862  1005 
fun do_introduce_combinators ctxt Ts t = 
42361  1006 
let val thy = Proof_Context.theory_of ctxt in 
43905
1ace987e22e5
avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns  this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents:
43864
diff
changeset

1007 
t > conceal_bounds Ts 
1ace987e22e5
avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns  this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents:
43864
diff
changeset

1008 
> cterm_of thy 
1ace987e22e5
avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns  this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents:
43864
diff
changeset

1009 
> Meson_Clausify.introduce_combinators_in_cterm 
1ace987e22e5
avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns  this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents:
43864
diff
changeset

1010 
> prop_of > Logic.dest_equals > snd 
1ace987e22e5
avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns  this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
blanchet
parents:
43864
diff
changeset

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

1012 
end 
43862  1013 
(* A type variable of sort "{}" will make abstraction fail. *) 
43997  1014 
handle THM _ => t > do_cheaply_conceal_lambdas Ts 
43862  1015 
val introduce_combinators = simple_translate_lambdas do_introduce_combinators 
1016 

43864
58a7b3fdc193
fixed lambdaliftg: must ensure the formulas are in close form
blanchet
parents:
43863
diff
changeset

1017 
fun preprocess_abstractions_in_terms trans_lambdas facts = 
43862  1018 
let 
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

1019 
val (facts, lambda_ts) = 
44501  1020 
facts > map (snd o snd) > trans_lambdas 
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

1021 
>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

1022 
val lambda_facts = 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

1023 
map2 (fn t => fn j => 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

1024 
((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t))) 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

1025 
lambda_ts (1 upto length lambda_ts) 
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

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

1027 

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

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

1029 
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

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

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

1032 
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

1033 
 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

1034 
 aux (Var ((s, i), T)) = 
43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

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

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

1037 
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

1038 

43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambdalifting (freshness of new names)
blanchet
parents:
43862
diff
changeset

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

1040 
let 
42361  1041 
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

1042 
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

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

1044 
> Object_Logic.atomize_term thy 
42563  1045 
val need_trueprop = (fastype_of t = @{typ bool}) 
43096  1046 
in 
1047 
t > need_trueprop ? HOLogic.mk_Trueprop 

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

1049 
> extensionalize_term ctxt 

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

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

1051 
> perhaps (try (HOLogic.dest_Trueprop)) 
43096  1052 
end 
1053 

1054 
(* making fact and conjecture formulas *) 

44495  1055 
fun make_formula thy format type_enc eq_as_iff name loc kind t = 
43096  1056 
let 
43859  1057 
val (iformula, atomic_types) = 
44495  1058 
iformula_from_prop thy format type_enc eq_as_iff (SOME (kind <> Conjecture)) t [] 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

1059 
in 
43859  1060 
{name = name, locality = loc, kind = kind, iformula = iformula, 
42562  1061 
atomic_types = atomic_types} 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

1063 

43860
57ef3cd4126e
more refactoring of preprocessing, so as to be able to centralize it
blanchet
parents:
43859
diff
changeset

1064 
fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) = 
43096  1065 
let val thy = Proof_Context.theory_of ctxt in 
44495  1066 
case t > make_formula thy format type_enc (eq_as_iff andalso format <> CNF) 
1067 
name loc Axiom of 

43859  1068 
formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => 
43096  1069 
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

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

1072 

44460  1073 
fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t 
1074 
 s_not_trueprop t = s_not t 

1075 

44463
c471a2b48fa1
make sure that all facts are passed to ATP from minimizer
blanchet
parents:
44460
diff
changeset

1076 
fun make_conjecture thy format type_enc = 
c471a2b48fa1
make sure that all facts are passed to ATP from minimizer
blanchet
parents:
44460
diff
changeset

1077 
map (fn ((name, loc), (kind, t)) => 
c471a2b48fa1
make sure that all facts are passed to ATP from minimizer
blanchet
parents:
44460
diff
changeset

1078 
t > kind = Conjecture ? s_not_trueprop 
44495  1079 
> make_formula thy format type_enc (format <> CNF) name loc kind) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

1080 

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

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

1082 

44399  1083 
type monotonicity_info = 
1084 
{maybe_finite_Ts : typ list, 

1085 
surely_finite_Ts : typ list, 

1086 
maybe_infinite_Ts : typ list, 

1087 
surely_infinite_Ts : typ list, 

1088 
maybe_nonmono_Ts : typ list} 

1089 

44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

1090 
(* These types witness that the type classes they belong to allow infinite 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

1091 
models and hence that any types with these type classes is monotonic. *) 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

1092 
val known_infinite_types = 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

1093 
[@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}] 
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

1094 

44500  1095 
fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T = 
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

1096 
soundness <> Sound andalso 
44500  1097 
is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T 
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

1098 

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

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

1100 
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

1101 
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

1102 
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

1103 

44399  1104 
fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true 
1105 
 should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, 

1106 
maybe_nonmono_Ts, ...} 

1107 
(Noninf_Nonmono_Types soundness) T = 

44491
ba22ed224b20
fixed bang encoding detection of which types to encode
blanchet
parents:
44463
diff
changeset

1108 
exists (type_intersect ctxt T) maybe_nonmono_Ts andalso 
44399  1109 
not (exists (type_instance ctxt T) surely_infinite_Ts orelse 
1110 
(not (member (type_aconv ctxt) maybe_finite_Ts T) andalso 

44500  1111 
is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T)) 
44399  1112 
 should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts, 
1113 
maybe_nonmono_Ts, ...} 

1114 
Fin_Nonmono_Types T = 

44491
ba22ed224b20
fixed bang encoding detection of which types to encode
blanchet
parents:
44463
diff
changeset

1115 
exists (type_intersect ctxt T) maybe_nonmono_Ts andalso 
ba22ed224b20
fixed bang encoding detection of which types to encode
blanchet
parents:
44463
diff
changeset

1116 
(exists (type_generalization ctxt T) surely_finite_Ts orelse 
44399  1117 
(not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso 
1118 
is_type_surely_finite ctxt 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

1119 
 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

1120 

44402  1121 
fun should_guard_type ctxt mono (Guards (_, level, uniformity)) should_guard_var 
44399  1122 
T = 
44402  1123 
(uniformity = Uniform orelse should_guard_var ()) andalso 
44399  1124 
should_encode_type ctxt mono level T 
1125 
 should_guard_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

1126 

44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

1127 
fun is_maybe_universal_var (IConst ((s, _), _, _)) = 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

1128 
String.isPrefix bound_var_prefix s orelse 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

1129 
String.isPrefix all_bound_var_prefix s 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

1130 
 is_maybe_universal_var (IVar _) = true 
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

1131 
 is_maybe_universal_var _ = false 
42836  1132 

43361
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1133 
datatype tag_site = 
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1134 
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

1135 
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

1136 
Elsewhere 
42829
1558741f8a72
started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents:
42828
diff
changeset

1137 

43361
e37b54d429f5
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
blanchet
parents:
43324
diff
changeset

1138 
fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false 
44402  1139 
 should_tag_with_type ctxt mono (Tags (_, level, uniformity)) site u T = 
1140 
(case uniformity of 

1141 
Uniform => should_encode_type ctxt mono level T 

1142 
 Nonuniform => 

44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

1143 
case (site, is_maybe_universal_var u) of 
44399  1144 
(Eq_Arg _, true) => should_encode_type ctxt mono level T 
42829
1558741f8a72
started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents:
42828
diff
changeset

1145 
 _ => false) 
1558741f8a72
started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents:
42828
diff
changeset

1146 
 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

1147 

44399  1148 
fun homogenized_type ctxt mono level = 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1149 
let 
44399  1150 
val should_encode = should_encode_type ctxt mono level 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1151 
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

1152 
 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

1153 
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

1154 
 homo _ _ = raise Fail "expected function type" 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1155 
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

1156 

44450
d848dd7b21f4
fixed "hBOOL" of existential variables, and generate more helpers
blanchet
parents:
44418
diff
changeset

1157 
(** predicators and application operators **) 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

1158 

42574  1159 
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

1160 
{pred_sym : bool, min_ary : int, max_ary : int, types : typ list} 
42563 