author  blanchet 
Thu, 02 Feb 2012 12:42:05 +0100  
changeset 46400  9ce354a77908 
parent 46399  338cf53508bc 
child 46402  ef8d65f64f77 
permissions  rwrr 
46320  1 
(* Title: HOL/Tools/ATP/atp_problem_generate.ML 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

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

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

5 

43863
a43d61270142
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of 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 

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

10 
sig 
43676
3b0b448b4d69
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes 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 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45299
diff
changeset

14 
type atp_format = ATP_Problem.atp_format 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

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

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

17 

46340  18 
datatype scope = Global  Local  Assum  Chained 
46393  19 
datatype status = General  Induct  Intro  Elim  Simp  Spec_Eq 
46340  20 
type stature = scope * status 
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 

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

22 
datatype polymorphism = Polymorphic  Raw_Monomorphic  Mangled_Monomorphic 
46301  23 
datatype strictness = Strict  Non_Strict 
44811  24 
datatype granularity = All_Vars  Positively_Naked_Vars  Ghost_Type_Arg_Vars 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of 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  
46301  27 
Noninf_Nonmono_Types of strictness * granularity  
44811  28 
Fin_Nonmono_Types of granularity  
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

29 
Const_Arg_Types  
43362  30 
No_Types 
44782  31 
type 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

32 

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

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

34 
val type_tag_arguments : bool Config.T 
45513
25388cf06437
rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents:
45511
diff
changeset

35 
val no_lamsN : string 
25388cf06437
rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents:
45511
diff
changeset

36 
val hide_lamsN : string 
46365  37 
val liftingN : string 
38 
val combsN : string 

39 
val combs_and_liftingN : string 

40 
val combs_or_liftingN : string 

45513
25388cf06437
rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents:
45511
diff
changeset

41 
val lam_liftingN : string 
25388cf06437
rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents:
45511
diff
changeset

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

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

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

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

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

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

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

49 
val class_prefix : string 
45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

50 
val lam_lifted_prefix : string 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

51 
val lam_lifted_mono_prefix : string 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

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

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

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

55 
val new_skolem_const_prefix : string 
45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

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

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

58 
val sym_decl_prefix : string 
43989  59 
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

60 
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

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

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

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

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

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

66 
val tfree_clause_prefix : string 
45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

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

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

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

70 
val type_tag_idempotence_helper_name : string 
42966
4e2d6c1e5392
more work on parsing 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 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45509
diff
changeset

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

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

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

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

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

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

88 
val atp_schematic_consts_of : term > typ list Symtab.table 
43828
e07a2c4cbad8
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
blanchet
parents:
43827
diff
changeset

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

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

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

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

93 
val is_type_enc_fairly_sound : type_enc > bool 
46301  94 
val type_enc_from_string : strictness > string > type_enc 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45299
diff
changeset

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

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

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

98 
val unmangled_const : string > string * (string, 'b) ho_term list 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

99 
val unmangled_const_name : string > string list 
43194  100 
val helper_table : ((string * bool) * thm list) list 
45514  101 
val trans_lams_from_string : 
102 
Proof.context > type_enc > string > term list > term list * term list 

43501
0e422a84d0b2
don't change the way helpers are generated for the exporter's sake
blanchet
parents:
43496
diff
changeset

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

104 
val prepare_atp_problem : 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45299
diff
changeset

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

106 
> bool > string > bool > bool > term list > term 
46340  107 
> ((string * stature) * term) list 
108 
> string problem * string Symtab.table * (string * stature) list vector 

45551  109 
* (string * term) list * int Symtab.table 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

110 
val atp_problem_weights : string problem > (string * real) list 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

112 

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

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

115 

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

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

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

118 

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

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

120 

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

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

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

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

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

125 

45516  126 
val no_lamsN = "no_lams" (* used internally; undocumented *) 
45513
25388cf06437
rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents:
45511
diff
changeset

127 
val hide_lamsN = "hide_lams" 
46365  128 
val liftingN = "lifting" 
129 
val combsN = "combs" 

130 
val combs_and_liftingN = "combs_and_lifting" 

131 
val combs_or_liftingN = "combs_or_lifting" 

45513
25388cf06437
rename the lambda translation schemes, so that they are understandable out of context
blanchet
parents:
45511
diff
changeset

132 
val keep_lamsN = "keep_lams" 
46365  133 
val lam_liftingN = "lam_lifting" (* legacy *) 
44088
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

134 

45779  135 
(* It's still unclear whether all TFF1 implementations will support type 
136 
signatures such as "!>[A : $tType] : $o", with ghost type variables. *) 

137 
val avoid_first_order_ghost_type_vars = false 

44622  138 

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

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

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

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

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

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

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

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

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

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

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

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

150 

45509  151 
(* Freshness almost guaranteed! *) 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

152 
val atp_prefix = "ATP" ^ Long_Name.separator 
45509  153 
val atp_weak_prefix = "ATP:" 
154 

45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

155 
val lam_lifted_prefix = atp_weak_prefix ^ "Lam" 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

156 
val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m" 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

157 
val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p" 
43907
073ab5379842
pass type arguments to lambdalifted Frees, to account for polymorphism
blanchet
parents:
43906
diff
changeset

158 

46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

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

160 
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

161 
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

162 

45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

163 
val combinator_prefix = "COMB" 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

164 

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

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

166 
val sym_decl_prefix = "sy_" 
43989  167 
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

168 
val tags_sym_formula_prefix = "tsy_" 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

169 
val app_op_alias_eq_prefix = "aa_" 
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

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

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

172 
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

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

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

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

176 

45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

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

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

179 
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

180 
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

181 

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

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

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

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

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

186 

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

188 
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

189 
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

190 

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

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

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

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

194 
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

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

197 

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

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

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

200 
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

201 

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

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

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

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

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

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

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

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

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

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

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

212 

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

213 
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

214 

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

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

216 

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

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

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

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

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

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

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

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

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

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

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

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

228 
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

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

230 
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

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

232 
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

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

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

235 
 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

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

237 

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

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

239 
unASCII'd. *) 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45509
diff
changeset

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

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

242 
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

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

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

245 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

259 
("equal", (@{const_name HOL.eq}, (@{thm fequal_def}, 
43678  260 
("fequal", @{const_name ATP.fequal})))), 
261 
("c_All", (@{const_name All}, (@{thm fAll_def}, 

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

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

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

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

265 

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

266 
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

267 

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

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

269 
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

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

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

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

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

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

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

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

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

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

279 
(@{const_name HOL.eq}, "equal"), 
43678  280 
(@{const_name All}, "All"), 
281 
(@{const_name Ex}, "Ex"), 

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

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

283 
(@{const_name Set.member}, "member"), 
45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

284 
(@{const_name Meson.COMBI}, combinator_prefix ^ "I"), 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

285 
(@{const_name Meson.COMBK}, combinator_prefix ^ "K"), 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

286 
(@{const_name Meson.COMBB}, combinator_prefix ^ "B"), 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

287 
(@{const_name Meson.COMBC}, combinator_prefix ^ "C"), 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

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

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

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

291 

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

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

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

294 
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

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

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

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

298 

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

299 
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

300 
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

301 

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

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

303 
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

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

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

306 

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

309 

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

310 
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

311 
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

312 
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

313 
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

314 
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

315 

43622  316 
fun make_schematic_type_var (x, i) = 
44595
444d111bde7d
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
blanchet
parents:
44594
diff
changeset

317 
tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i)) 
43622  318 
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

319 

45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45299
diff
changeset

320 
(* "HOL.eq" and choice are mapped to the ATP's equivalents *) 
44587  321 
local 
322 
val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT 

323 
fun default c = const_prefix ^ lookup_const c 

324 
in 

325 
fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal 

44754  326 
 make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c = 
327 
if c = choice_const then tptp_choice else default c 

44587  328 
 make_fixed_const _ c = default c 
329 
end 

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

330 

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

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

332 

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

333 
fun make_type_class clas = class_prefix ^ ascii_of clas 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

334 

43093  335 
fun new_skolem_var_name_from_const s = 
336 
let val ss = s > space_explode Long_Name.separator in 

337 
nth ss (length ss  2) 

338 
end 

339 

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

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

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

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

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

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

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

346 

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

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

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

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

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

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

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

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

354 

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

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

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

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

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

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

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

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

362 
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

363 

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

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

365 

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

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

367 

44625  368 
type arity_atom = name * name * name list 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

369 

43263  370 
val type_class = the_single @{sort type} 
371 

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

373 
{name : string, 
44625  374 
prem_atoms : arity_atom list, 
375 
concl_atom : arity_atom} 

376 

377 
fun add_prem_atom tvar = 

378 
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

379 

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

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

381 
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

382 
let 
44595
444d111bde7d
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
blanchet
parents:
44594
diff
changeset

383 
val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args) 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

385 
in 
43086  386 
{name = name, 
44625  387 
prem_atoms = [] > fold (uncurry add_prem_atom) tvars_srts, 
388 
concl_atom = (`make_type_class cls, `make_fixed_type_const tcons, 

389 
tvars ~~ tvars)} 

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

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

391 

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

392 
fun arity_clause _ _ (_, []) = [] 
43495  393 
 arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *) 
394 
arity_clause seen n (tcons, ars) 

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

396 
if member (op =) seen class then 

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

398 
make_axiom_arity_clause (tcons, 

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

400 
ar) :: 

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

402 
else 

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

404 
ascii_of class, ar) :: 

405 
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

406 

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

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

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

410 

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

413 
fun type_class_pairs thy tycons classes = 
43093  414 
let 
415 
val alg = Sign.classes_of thy 

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

417 
fun add_class tycon class = 

418 
cons (class, domain_sorts tycon class) 

419 
handle Sorts.CLASS_ERROR _ => I 

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

421 
in map try_classes tycons end 

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

422 

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

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

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

425 
 iter_type_class_pairs thy tycons classes = 
43263  426 
let 
427 
fun maybe_insert_class s = 

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

429 
? insert (op =) s 

430 
val cpairs = type_class_pairs thy tycons classes 

431 
val newclasses = 

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

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

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

435 

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

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

437 
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

438 

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 
(** Isabelle class relations **) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

441 

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

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

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

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

446 

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

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

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

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

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

452 
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

453 
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

454 
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

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

456 

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

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

460 

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

461 
fun make_class_rel_clauses thy subs supers = 
43093  462 
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

463 

43859  464 
(* intermediate terms *) 
465 
datatype iterm = 

466 
IConst of name * typ * typ list  

467 
IVar of name * typ  

468 
IApp of iterm * iterm  

469 
IAbs of (name * typ) * iterm 

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

470 

43859  471 
fun ityp_of (IConst (_, T, _)) = T 
472 
 ityp_of (IVar (_, T)) = T 

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

474 
 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

475 

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

476 
(*gets the head of a combinator application, along with the list of arguments*) 
43859  477 
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

478 
let 
43859  479 
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

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

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

482 

45316
08d84bdd5b37
improve handling of bound type variables (esp. for TFF1)
blanchet
parents:
45315
diff
changeset

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

484 

45509  485 
val tvar_a_str = "'a" 
486 
val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS) 

487 
val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str) 

488 
val itself_name = `make_fixed_type_const @{type_name itself} 

489 
val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE} 

490 
val tvar_a_atype = AType (tvar_a_name, []) 

491 
val a_itself_atype = AType (itself_name, [tvar_a_atype]) 

492 

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

493 
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

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

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

496 

44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

497 
fun robust_const_type thy s = 
45509  498 
if s = app_op_name then 
499 
Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"} 

45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

500 
else if String.isPrefix lam_lifted_prefix s then 
45509  501 
Logic.varifyT_global @{typ "'a => 'b"} 
502 
else 

503 
(* Old Skolems throw a "TYPE" exception here, which will be caught. *) 

504 
s > Sign.the_const_type thy 

44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

505 

ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

506 
(* This function only makes sense if "T" is as general as possible. *) 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

507 
fun robust_const_typargs thy (s, T) = 
45509  508 
if s = app_op_name then 
509 
let val (T1, T2) = T > domain_type > dest_funT in [T1, T2] end 

510 
else if String.isPrefix old_skolem_const_prefix s then 

511 
[] > Term.add_tvarsT T > rev > map TVar 

45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

512 
else if String.isPrefix lam_lifted_prefix s then 
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

513 
if String.isPrefix lam_lifted_poly_prefix s then 
45511
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45509
diff
changeset

514 
let val (T1, T2) = T > dest_funT in [T1, T2] end 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45509
diff
changeset

515 
else 
9b0f8ca4388e
continued implementation of lambdalifting in Metis
blanchet
parents:
45509
diff
changeset

516 
[] 
45509  517 
else 
518 
(s, T) > Sign.const_typargs thy 

44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

519 

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

44495  522 
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

523 
let 
44495  524 
val (P', P_atomics_Ts) = iterm_from_term thy format bs P 
525 
val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q 

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

44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

529 
robust_const_typargs thy (c, T)), 
45316
08d84bdd5b37
improve handling of bound type variables (esp. for TFF1)
blanchet
parents:
45315
diff
changeset

530 
atomic_types_of T) 
44495  531 
 iterm_from_term _ _ _ (Free (s, T)) = 
45509  532 
(IConst (`make_fixed_var s, T, []), atomic_types_of T) 
44495  533 
 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

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

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

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

537 
val s' = new_skolem_const_name s (length Ts) 
44495  538 
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

539 
else 
45316
08d84bdd5b37
improve handling of bound type variables (esp. for TFF1)
blanchet
parents:
45315
diff
changeset

540 
IVar ((make_schematic_var v, s), T), atomic_types_of T) 
44495  541 
 iterm_from_term _ _ bs (Bound j) = 
45316
08d84bdd5b37
improve handling of bound type variables (esp. for TFF1)
blanchet
parents:
45315
diff
changeset

542 
nth bs j > (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T)) 
44495  543 
 iterm_from_term thy format bs (Abs (s, T, t)) = 
43678  544 
let 
545 
fun vary s = s > AList.defined (op =) bs s ? vary o Symbol.bump_string 

546 
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

547 
val name = `make_bound_var s 
44495  548 
val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t 
45316
08d84bdd5b37
improve handling of bound type variables (esp. for TFF1)
blanchet
parents:
45315
diff
changeset

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

550 

46340  551 
datatype scope = Global  Local  Assum  Chained 
46393  552 
datatype status = General  Induct  Intro  Elim  Simp  Spec_Eq 
46340  553 
type stature = scope * status 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

554 

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

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

556 
datatype polymorphism = Polymorphic  Raw_Monomorphic  Mangled_Monomorphic 
46301  557 
datatype strictness = Strict  Non_Strict 
44811  558 
datatype granularity = All_Vars  Positively_Naked_Vars  Ghost_Type_Arg_Vars 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

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

560 
All_Types  
46301  561 
Noninf_Nonmono_Types of strictness * granularity  
44811  562 
Fin_Nonmono_Types of granularity  
44397
06375952f1fa
cleaner handling of polymorphic monotonicity inference
blanchet
parents:
44396
diff
changeset

563 
Const_Arg_Types  
43362  564 
No_Types 
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

565 

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

566 
datatype type_enc = 
44591
0b107d11f634
extended simple types with polymorphism  the implementation still needs some work though
blanchet
parents:
44589
diff
changeset

567 
Simple_Types of order * polymorphism * type_level  
44768  568 
Guards of polymorphism * type_level  
569 
Tags of polymorphism * type_level 

570 

571 
fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true 

572 
 is_type_enc_higher_order _ = false 

573 

574 
fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly 

575 
 polymorphism_of_type_enc (Guards (poly, _)) = poly 

576 
 polymorphism_of_type_enc (Tags (poly, _)) = poly 

577 

578 
fun level_of_type_enc (Simple_Types (_, _, level)) = level 

579 
 level_of_type_enc (Guards (_, level)) = level 

580 
 level_of_type_enc (Tags (_, level)) = level 

581 

44811  582 
fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain 
583 
 granularity_of_type_level (Fin_Nonmono_Types grain) = grain 

584 
 granularity_of_type_level _ = All_Vars 

44768  585 

586 
fun is_type_level_quasi_sound All_Types = true 

587 
 is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true 

588 
 is_type_level_quasi_sound _ = false 

589 
val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc 

590 

591 
fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true 

592 
 is_type_level_fairly_sound level = is_type_level_quasi_sound level 

593 
val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc 

594 

595 
fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true 

596 
 is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true 

597 
 is_type_level_monotonicity_based _ = false 

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

598 

44785  599 
(* "_query", "_bang", and "_at" are for the ASCIIchallenged Metis and 
600 
Mirabelle. *) 

601 
val queries = ["?", "_query"] 

602 
val bangs = ["!", "_bang"] 

603 
val ats = ["@", "_at"] 

604 

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

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

606 
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

607 

44785  608 
fun try_nonmono constr suffixes fallback s = 
609 
case try_unsuffixes suffixes s of 

610 
SOME s => 

611 
(case try_unsuffixes suffixes s of 

44811  612 
SOME s => (constr Positively_Naked_Vars, s) 
44785  613 
 NONE => 
614 
case try_unsuffixes ats s of 

44811  615 
SOME s => (constr Ghost_Type_Arg_Vars, s) 
616 
 NONE => (constr All_Vars, s)) 

44785  617 
 NONE => fallback s 
44768  618 

46301  619 
fun type_enc_from_string strictness s = 
42722  620 
(case try (unprefix "poly_") s of 
621 
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

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

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

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

626 
case try (unprefix "mono_") s of 
42722  627 
SOME s => (SOME Mangled_Monomorphic, s) 
628 
 NONE => (NONE, s)) 

44785  629 
> (pair All_Types 
630 
> try_nonmono Fin_Nonmono_Types bangs 

46301  631 
> try_nonmono (curry Noninf_Nonmono_Types strictness) queries) 
44768  632 
> (fn (poly, (level, core)) => 
633 
case (core, (poly, level)) of 

634 
("simple", (SOME poly, _)) => 

44742  635 
(case (poly, level) of 
636 
(Polymorphic, All_Types) => 

637 
Simple_Types (First_Order, Polymorphic, All_Types) 

638 
 (Mangled_Monomorphic, _) => 

44811  639 
if granularity_of_type_level level = All_Vars then 
44768  640 
Simple_Types (First_Order, Mangled_Monomorphic, level) 
641 
else 

642 
raise Same.SAME 

44742  643 
 _ => raise Same.SAME) 
44768  644 
 ("simple_higher", (SOME poly, _)) => 
44591
0b107d11f634
extended simple types with polymorphism  the implementation still needs some work though
blanchet
parents:
44589
diff
changeset

645 
(case (poly, level) of 
44754  646 
(Polymorphic, All_Types) => 
647 
Simple_Types (Higher_Order, Polymorphic, All_Types) 

648 
 (_, Noninf_Nonmono_Types _) => raise Same.SAME 

44742  649 
 (Mangled_Monomorphic, _) => 
44811  650 
if granularity_of_type_level level = All_Vars then 
44768  651 
Simple_Types (Higher_Order, Mangled_Monomorphic, level) 
652 
else 

653 
raise Same.SAME 

44742  654 
 _ => raise Same.SAME) 
44810  655 
 ("guards", (SOME poly, _)) => 
45949
70b9d1e9fddc
killed "guard@?" encodings  they were found to be unsound
blanchet
parents:
45948
diff
changeset

656 
if poly = Mangled_Monomorphic andalso 
70b9d1e9fddc
killed "guard@?" encodings  they were found to be unsound
blanchet
parents:
45948
diff
changeset

657 
granularity_of_type_level level = Ghost_Type_Arg_Vars then 
70b9d1e9fddc
killed "guard@?" encodings  they were found to be unsound
blanchet
parents:
45948
diff
changeset

658 
raise Same.SAME 
70b9d1e9fddc
killed "guard@?" encodings  they were found to be unsound
blanchet
parents:
45948
diff
changeset

659 
else 
70b9d1e9fddc
killed "guard@?" encodings  they were found to be unsound
blanchet
parents:
45948
diff
changeset

660 
Guards (poly, level) 
44810  661 
 ("tags", (SOME poly, _)) => 
45949
70b9d1e9fddc
killed "guard@?" encodings  they were found to be unsound
blanchet
parents:
45948
diff
changeset

662 
if granularity_of_type_level level = Ghost_Type_Arg_Vars then 
70b9d1e9fddc
killed "guard@?" encodings  they were found to be unsound
blanchet
parents:
45948
diff
changeset

663 
raise Same.SAME 
70b9d1e9fddc
killed "guard@?" encodings  they were found to be unsound
blanchet
parents:
45948
diff
changeset

664 
else 
70b9d1e9fddc
killed "guard@?" encodings  they were found to be unsound
blanchet
parents:
45948
diff
changeset

665 
Tags (poly, level) 
44768  666 
 ("args", (SOME poly, All_Types (* naja *))) => 
667 
Guards (poly, Const_Arg_Types) 

668 
 ("erased", (NONE, All_Types (* naja *))) => 

669 
Guards (Polymorphic, No_Types) 

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

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

672 

44754  673 
fun adjust_type_enc (THF (TPTP_Monomorphic, _, _)) 
674 
(Simple_Types (order, _, level)) = 

44591
0b107d11f634
extended simple types with polymorphism  the implementation still needs some work though
blanchet
parents:
44589
diff
changeset

675 
Simple_Types (order, Mangled_Monomorphic, level) 
44754  676 
 adjust_type_enc (THF _) type_enc = type_enc 
677 
 adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) = 

44591
0b107d11f634
extended simple types with polymorphism  the implementation still needs some work though
blanchet
parents:
44589
diff
changeset

678 
Simple_Types (First_Order, Mangled_Monomorphic, level) 
45303
bd03b08161ac
added DFG unsorted support (like in the old days)
blanchet
parents:
45301
diff
changeset

679 
 adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) = 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45299
diff
changeset

680 
Simple_Types (First_Order, Mangled_Monomorphic, level) 
44754  681 
 adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) = 
44591
0b107d11f634
extended simple types with polymorphism  the implementation still needs some work though
blanchet
parents:
44589
diff
changeset

682 
Simple_Types (First_Order, poly, level) 
0b107d11f634
extended simple types with polymorphism  the implementation still needs some work though
blanchet
parents:
44589
diff
changeset

683 
 adjust_type_enc format (Simple_Types (_, poly, level)) = 
44768  684 
adjust_type_enc format (Guards (poly, level)) 
44416
cabd06b69c18
added formats to the slice and use TFF for remote Vampire
blanchet
parents:
44410
diff
changeset

685 
 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

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

687 
 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

688 

45509  689 
fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u 
690 
 constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t) 

691 
 constify_lifted (Free (x as (s, _))) = 

45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

692 
(if String.isPrefix lam_lifted_prefix s then Const else Free) x 
45509  693 
 constify_lifted t = t 
694 

46375
d724066ff3d0
reverted e2b1a86d59fc  broke Metis's lambdalifting
blanchet
parents:
46371
diff
changeset

695 
(* Requires bound variables not to clash with any schematic variables (as should 
d724066ff3d0
reverted e2b1a86d59fc  broke Metis's lambdalifting
blanchet
parents:
46371
diff
changeset

696 
be the case right after lambdalifting). *) 
46385
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

697 
fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) = 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

698 
(case try unprefix s of 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

699 
SOME s => 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

700 
let 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

701 
val names = Name.make_context (map fst (Term.add_var_names t' [])) 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

702 
val (s, _) = Name.variant s names 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

703 
in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

704 
 NONE => t) 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

705 
 open_form _ t = t 
46375
d724066ff3d0
reverted e2b1a86d59fc  broke Metis's lambdalifting
blanchet
parents:
46371
diff
changeset

706 

45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

707 
fun lift_lams_part_1 ctxt type_enc = 
45568
211a6e6cbc04
move etacontraction to before translation to Metis, to ensure everything stays in sync
blanchet
parents:
45565
diff
changeset

708 
map close_form #> rpair ctxt 
44088
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

709 
#> Lambda_Lifting.lift_lambdas 
45564  710 
(SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then 
711 
lam_lifted_poly_prefix 

712 
else 

713 
lam_lifted_mono_prefix) ^ "_a")) 

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

714 
Lambda_Lifting.is_quantifier 
45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

715 
#> fst 
46385
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

716 
fun lift_lams_part_2 (facts, lifted) = 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

717 
(map (open_form (unprefix close_form_prefix) o constify_lifted) facts, 
0ccf458a3633
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet
parents:
46384
diff
changeset

718 
map (open_form I o constify_lifted) lifted) 
45554
09ad83de849c
don't pass "lam_lifted" option to "metis" unless there's a good reason
blanchet
parents:
45551
diff
changeset

719 
val lift_lams = lift_lams_part_2 ooo lift_lams_part_1 
44088
3693baa6befb
move lambdalifting code to ATP encoding, so it can be used by Metis
blanchet
parents:
44003
diff
changeset

720 

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

721 
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

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

723 
 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

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

725 
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

726 
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

727 
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

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

729 
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

730 
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

731 
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

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

733 

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

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

737 
kind : formula_kind, 
43859  738 
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

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

740 

46340  741 
fun update_iformula f ({name, stature, kind, iformula, atomic_types} 
43859  742 
: translated_formula) = 
46340  743 
{name = name, stature = stature, kind = kind, iformula = f iformula, 
42562  744 
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

745 

43859  746 
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

747 

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

748 
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

749 
let val T = get_T x in 
44399  750 
if exists (type_instance ctxt T o get_T) xs then xs 
751 
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

752 
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

753 

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

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

755 
datatype type_arg_policy = 
45937  756 
Explicit_Type_Args of bool (* infer_from_term_args *)  
44771  757 
Mangled_Type_Args  
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

758 
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

759 

45945
aa8100cc02dc
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents:
45939
diff
changeset

760 
fun type_arg_policy monom_constrs type_enc s = 
45315  761 
let val poly = polymorphism_of_type_enc type_enc in 
44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

762 
if s = type_tag_name then 
45315  763 
if poly = Mangled_Monomorphic then Mangled_Type_Args 
764 
else Explicit_Type_Args false 

44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

765 
else case type_enc of 
45315  766 
Simple_Types (_, Polymorphic, _) => Explicit_Type_Args false 
767 
 Tags (_, All_Types) => No_Type_Args 

44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

768 
 _ => 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

769 
let val level = level_of_type_enc type_enc in 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

770 
if level = No_Types orelse s = @{const_name HOL.eq} orelse 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

771 
(s = app_op_name andalso level = Const_Arg_Types) then 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

772 
No_Type_Args 
45315  773 
else if poly = Mangled_Monomorphic then 
44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

774 
Mangled_Type_Args 
45945
aa8100cc02dc
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents:
45939
diff
changeset

775 
else if member (op =) monom_constrs s andalso 
aa8100cc02dc
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents:
45939
diff
changeset

776 
granularity_of_type_level level = Positively_Naked_Vars then 
aa8100cc02dc
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents:
45939
diff
changeset

777 
No_Type_Args 
44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

778 
else 
44811  779 
Explicit_Type_Args 
780 
(level = All_Types orelse 

781 
granularity_of_type_level level = Ghost_Type_Arg_Vars) 

44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

782 
end 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

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

784 

44625  785 
(* Make atoms for sorted type variables. *) 
43263  786 
fun generic_add_sorts_on_type (_, []) = I 
787 
 generic_add_sorts_on_type ((x, i), s :: ss) = 

788 
generic_add_sorts_on_type ((x, i), ss) 

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

43093  790 
I 
791 
else if i = ~1 then 

44623  792 
insert (op =) (`make_type_class s, `make_fixed_type_var x) 
43093  793 
else 
44623  794 
insert (op =) (`make_type_class s, 
795 
(make_schematic_type_var (x, i), x))) 

43263  796 
fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S) 
797 
 add_sorts_on_tfree _ = I 

798 
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z 

799 
 add_sorts_on_tvar _ = I 

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

800 

44625  801 
fun type_class_formula type_enc class arg = 
802 
AAtom (ATerm (class, arg :: 

803 
(case type_enc of 

44754  804 
Simple_Types (First_Order, Polymorphic, _) => 
45301
866b075aa99b
added sorted DFG output for coming version of SPASS
blanchet
parents:
45299
diff
changeset

805 
if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])] 
44754  806 
else [] 
44625  807 
 _ => []))) 
808 
fun formulas_for_types type_enc add_sorts_on_typ Ts = 

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

809 
[] > level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts 
44625  810 
> map (fn (class, name) => 
811 
type_class_formula type_enc class (ATerm (name, []))) 

41137
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

812 

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

813 
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

814 
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

815 
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

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

817 
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

818 
 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

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

820 
 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

821 
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

822 
 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

823 

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

825 
let 
45315  826 
fun add_formula_vars bounds (AQuant (_, xs, phi)) = 
827 
add_formula_vars (map fst xs @ bounds) phi 

828 
 add_formula_vars bounds (AConn (_, phis)) = 

829 
fold (add_formula_vars bounds) phis 

830 
 add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm 

831 
in mk_aquant AForall (add_formula_vars [] phi []) phi end 

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

832 

45377  833 
fun add_term_vars bounds (ATerm (name as (s, _), tms)) = 
834 
(if is_tptp_variable s andalso 

835 
not (String.isPrefix tvar_prefix s) andalso 

836 
not (member (op =) bounds name) then 

837 
insert (op =) (name, NONE) 

838 
else 

839 
I) 

840 
#> fold (add_term_vars bounds) tms 

841 
 add_term_vars bounds (AAbs ((name, _), tm)) = 

842 
add_term_vars (name :: bounds) tm 

45401  843 
fun close_formula_universally phi = close_universally add_term_vars phi 
45315  844 

845 
fun add_iterm_vars bounds (IApp (tm1, tm2)) = 

846 
fold (add_iterm_vars bounds) [tm1, tm2] 

847 
 add_iterm_vars _ (IConst _) = I 

848 
 add_iterm_vars bounds (IVar (name, T)) = 

849 
not (member (op =) bounds name) ? insert (op =) (name, SOME T) 

850 
 add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm 

851 
fun close_iformula_universally phi = close_universally add_iterm_vars phi 

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

852 

46338
b02ff6b17599
better handling of individual type for DFG format (SPASS)
blanchet
parents:
46320
diff
changeset

853 
val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *) 
44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

854 
val fused_infinite_type = Type (fused_infinite_type_name, []) 
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

855 

ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

856 
fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s) 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

857 

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

858 
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

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

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

861 
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

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

863 
 (true, @{type_name fun}) => `I tptp_fun_type 
44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

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

865 
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

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

867 
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

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

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

870 
 term (TFree (s, _)) = ATerm (`make_fixed_type_var s, []) 
44594
ae82943481e9
added type abstractions (for declaring polymorphic constants) to TFF syntax
blanchet
parents:
44593
diff
changeset

871 
 term (TVar (x, _)) = ATerm (tvar_name x, []) 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

872 
in term end 
42562  873 

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

874 
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

875 
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

876 

42562  877 
(* This shouldn't clash with anything else. *) 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

878 
val app_op_alias_sep = "\000" 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

879 
val mangled_type_sep = "\001" 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

880 

676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

881 
val ascii_of_app_op_alias_sep = ascii_of app_op_alias_sep 
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

882 

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

885 
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

886 
^ ")" 
43692  887 
 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

888 

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

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

890 
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

891 

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

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

893 
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

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

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

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

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

898 

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

899 
fun ho_type_from_ho_term type_enc pred_sym ary = 
42963  900 
let 
44593
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44591
diff
changeset

901 
fun to_mangled_atype ty = 
42963  902 
AType ((make_simple_type (generic_mangled_type_name fst ty), 
44593
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44591
diff
changeset

903 
generic_mangled_type_name snd ty), []) 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44591
diff
changeset

904 
fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys) 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44591
diff
changeset

905 
 to_poly_atype _ = raise Fail "unexpected type abstraction" 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44591
diff
changeset

906 
val to_atype = 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44591
diff
changeset

907 
if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype 
ccf40af26ae9
implement more of the polymorphic simply typed format TFF(1)
blanchet
parents:
44591
diff
changeset

908 
else to_mangled_atype 
42963  909 
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

910 
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

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

913 
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

914 
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

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

916 
in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end 
42963  917 

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

919 
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

920 
o ho_term_from_typ format type_enc 
42963  921 

46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

922 
fun aliased_app_op ary (s, s') = 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

923 
(s ^ ascii_of_app_op_alias_sep ^ string_of_int ary, s' ^ string_of_int ary) 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

924 
fun unaliased_app_op (s, s') = 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

925 
case space_explode app_op_alias_sep s of 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

926 
[_] => (s, s') 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

927 
 [s1, s2] => (s1, unsuffix s2 s') 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

928 
 _ => raise Fail "illformed explicit application alias" 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

929 

676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

930 
fun raw_mangled_const_name type_name ty_args (s, s') = 
42963  931 
let 
932 
fun type_suffix f g = 

46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

933 
fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f) 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

934 
ty_args "" 
42963  935 
in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

936 
fun mangled_const_name format type_enc = 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

937 
map_filter (ho_term_for_type_arg format type_enc) 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

938 
#> raw_mangled_const_name generic_mangled_type_name 
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

939 

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

940 
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

941 
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

942 

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

943 
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

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

945 
 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

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

947 
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

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

949 

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

950 
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

951 
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

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

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

954 
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

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

956 

46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

957 
fun unmangled_const_name s = 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

958 
(s, s) > unaliased_app_op > fst > space_explode mangled_type_sep 
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

959 
fun unmangled_const s = 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

960 
let val ss = unmangled_const_name s in 
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

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

962 
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

963 

44773
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

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

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

966 
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

967 
 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

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

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

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

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

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

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

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

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

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

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

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

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

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

981 
 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

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

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

984 
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

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

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

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

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

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

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

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

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

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

994 
 (false, s) => 
44097  995 
if is_tptp_equal s andalso length args = 2 then 
996 
IConst (`I tptp_equal, T, []) 

997 
else 

44589
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44587
diff
changeset

998 
(* Use a proxy even for partially applied THF0 equality, 
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44587
diff
changeset

999 
because the LEOII and Satallax parsers complain about not 
0a1dfc6365e9
first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents:
44587
diff
changeset

1000 
being able to infer the type of "=". *) 
44097  1001 
IConst (proxy_base >> prefix const_prefix, T, T_args) 
43987
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

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

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

1004 
IConst (proxy_base >> prefix const_prefix, T, T_args) 
45167
6bc8d260d459
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambdaabstraction in higherorder translations
blanchet
parents:
44859
diff
changeset

1005 
 NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args 
6bc8d260d459
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambdaabstraction in higherorder translations
blanchet
parents:
44859
diff
changeset

1006 
else IConst (name, T, T_args)) 
43987
2850b7dc27a4
further worked around LEOII parser limitation, with etaexpansion
blanchet
parents:
43985
diff
changeset

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

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

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

1010 

46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1011 
fun mangle_type_args_in_const format type_enc (name as (s, _)) T_args = 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1012 
case unprefix_and_unascii const_prefix s of 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1013 
NONE => (name, T_args) 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1014 
 SOME s'' => 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1015 
case type_arg_policy [] type_enc (invert_const s'') of 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1016 
Mangled_Type_Args => (mangled_const_name format type_enc T_args name, []) 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1017 
 _ => (name, T_args) 
44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1018 
fun mangle_type_args_in_iterm format type_enc = 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1019 
if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1020 
let 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1021 
fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2) 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1022 
 mangle (tm as IConst (_, _, [])) = tm 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1023 
 mangle (IConst (name, T, T_args)) = 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1024 
mangle_type_args_in_const format type_enc name T_args 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1025 
> (fn (name, T_args) => IConst (name, T, T_args)) 
44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1026 
 mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm) 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1027 
 mangle tm = tm 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1028 
in mangle end 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1029 
else 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1030 
I 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1031 

44773
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1032 
fun chop_fun 0 T = ([], T) 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1033 
 chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1034 
chop_fun (n  1) ran_T >> cons dom_T 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1035 
 chop_fun _ T = ([], T) 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1036 

44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1037 
fun filter_const_type_args _ _ _ [] = [] 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1038 
 filter_const_type_args thy s ary T_args = 
44773
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1039 
let 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1040 
val U = robust_const_type thy s 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1041 
val arg_U_vars = fold Term.add_tvarsT (U > chop_fun ary > fst) [] 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1042 
val U_args = (s, U) > robust_const_typargs thy 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1043 
in 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1044 
U_args ~~ T_args 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1045 
> map (fn (U, T) => 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1046 
if member (op =) arg_U_vars (dest_TVar U) then dummyT else T) 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1047 
end 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1048 
handle TYPE _ => T_args 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1049 

46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1050 
fun filter_type_args_in_const _ _ _ _ _ [] = [] 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1051 
 filter_type_args_in_const thy monom_constrs type_enc ary s T_args = 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1052 
case unprefix_and_unascii const_prefix s of 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1053 
NONE => 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1054 
if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then [] 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1055 
else T_args 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1056 
 SOME s'' => 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1057 
let 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1058 
val s'' = invert_const s'' 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1059 
fun filter_T_args false = T_args 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1060 
 filter_T_args true = filter_const_type_args thy s'' ary T_args 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1061 
in 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1062 
case type_arg_policy monom_constrs type_enc s'' of 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1063 
Explicit_Type_Args infer_from_term_args => 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1064 
filter_T_args infer_from_term_args 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1065 
 No_Type_Args => [] 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1066 
 Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol" 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1067 
end 
45945
aa8100cc02dc
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
blanchet
parents:
45939
diff
changeset

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

1069 
let 
44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1070 
fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2) 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1071 
 filt ary (IConst (name as (s, _), T, T_args)) = 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1072 
filter_type_args_in_const thy monom_constrs type_enc ary s T_args 
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1073 
> (fn T_args => IConst (name, T, T_args)) 
44774
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1074 
 filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm) 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1075 
 filt _ tm = tm 
72785558a6ff
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
blanchet
parents:
44773
diff
changeset

1076 
in filt 0 end 
44773
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1077 

e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1078 
fun iformula_from_prop ctxt format type_enc eq_as_iff = 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1079 
let 
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1080 
val thy = Proof_Context.theory_of ctxt 
45316
08d84bdd5b37
improve handling of bound type variables (esp. for TFF1)
blanchet
parents:
45315
diff
changeset

1081 
fun do_term bs t atomic_Ts = 
44495  1082 
iterm_from_term thy format bs (Envir.eta_contract t) 
44773
e701dabbfe37
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
blanchet
parents:
44772
diff
changeset

1083 
>> (introduce_proxies_in_iterm type_enc 
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46389
diff
changeset

1084 
#> mangle_type_args_in_iterm format type_enc #> AAtom) 
45316
08d84bdd5b37
improve handling of bound type variables (esp. for TFF1)
blanchet
parents:
45315
diff
changeset

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

1086 
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

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

1088 
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

1089 
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

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

1091 
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

1092 
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

1093 
 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

1094 
 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

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

1096 
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

1097 
#>> mk_aquant q [(name, SOME T)] 
45316
08d84bdd5b37
improve handling of bound type variables (esp. for TFF1)
blanchet
parents:
45315
diff
changeset

1098 
##> union (op =) (atomic_types_of T) 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

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

1100 
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

1101 
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

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

1103 
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

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

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

1106 
 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

1107 
do_quant bs AForall pos s T t' 
45167
6bc8d260d459
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambdaabstraction in higherorder translations
blanchet
parents:
44859
diff
changeset

1108 
 (t0 as Const (@{const_name All}, _)) $ t1 => 
6bc8d260d459
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambdaabstraction in higherorder translations
blanchet
parents:
44859
diff
changeset

1109 
do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

1110 
 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

1111 
do_quant bs AExists pos s T t' 
45167
6bc8d260d459
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambdaabstraction in higherorder translations
blanchet
parents:
44859
diff
changeset

1112 
 (t0 as Const (@{const_name Ex}, _)) $ t1 => 
6bc8d260d459
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambdaabstraction in higherorder translations
blanchet
parents:
44859
diff
changeset

1113 
do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1) 
44403
15160cdc4688
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
blanchet
parents:
44402
diff
changeset

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

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

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

1117 
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

1118 
 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

1119 
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

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

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

1122 

46093  1123 
fun presimplify_term ctxt t = 
1124 
t > exists_Const (member (op =) Meson.presimplified_consts o fst) t 

1125 
? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) 

1126 
#> Meson.presimplify 

1127 
#> prop_of) 

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

1128 

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

1129 
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

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

1131 
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

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

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

1134 
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

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

1136 

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

1139 
 is_fun_equality _ = false 

1140 

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

1141 
fun extensionalize_term ctxt t = 
43265  1142 
if exists_Const is_fun_equality t then 
1143 
let val thy = Proof_Context.theory_of ctxt in 

1144 
t > cterm_of thy > Meson.extensionalize_conv ctxt 

1145 
> prop_of > Logic.dest_equals > snd 

1146 
end 

1147 
else 

1148 
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

1149 

43862  1150 
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

1151 
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

1152 
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

1153 
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

1154 
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

1155 
let 
44814
52318464c73b
also implemented ghost version of the tagged encodings
blanchet
parents:
44812
diff
changeset

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

1157 
case t of 
44814
52318464c73b
also implemented ghost version of the tagged encodings
blanchet
parents:
44812
diff
changeset

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

1159 
 (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => 
44814
52318464c73b
also implemented ghost version of the tagged encodings
blanchet
parents:
44812
diff
changeset

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

1161 
 (t0 as Const (@{const_name All}, _)) $ t1 => 
44814
52318464c73b
also implemented ghost version of the tagged encodings
blanchet
parents:
44812
diff
changeset

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

1163 
 (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => 
44814
52318464c73b
also implemented ghost version of the tagged encodings
blanchet
parents:
44812
diff
changeset

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

1165 
 (t0 as Const (@{const_name Ex}, _)) $ t1 => 
44814
52318464c73b
also implemented ghost version of the tagged encodings
blanchet
parents:
44812
diff
changeset

1166 
trans Ts (t0 $ eta_expand Ts t1 1) 
52318464c73b
also implemented ghost version of the tagged encodings
blanchet
parents:
44812
diff
changeset

1167 
 (t0 as @{const HOL.conj}) $ t1 $ t2 => 
52318464c73b
also implemented ghost version of the tagged encodings
blanchet
parents:
44812
diff
changeset

1168 
t0 $ trans Ts t1 $ trans Ts t2 
52318464c73b
also implemented ghost version of the tagged encodings
blanchet
parents:
44812
diff
changeset

1169 
 (t0 as @{const HOL.disj}) $ t1 $ t2 => 