author  blanchet 
Mon, 06 Jun 2011 20:36:35 +0200  
changeset 43181  cd3b7798ecc2 
parent 43179  db5fb1d4df42 
child 43185  697d32fa183d 
permissions  rwrr 
40114  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

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

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

5 

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

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

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

8 

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

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

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

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

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

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

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

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

17 

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

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

19 

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

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

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

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

23 

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

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

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

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

27 

43086  28 
type arity_clause = 
29 
{name: string, 

30 
prem_lits: arity_literal list, 

31 
concl_lits: arity_literal} 

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

32 

43086  33 
type class_rel_clause = 
34 
{name: string, 

35 
subclass: name, 

36 
superclass: name} 

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

37 

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

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

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

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

41 
CombApp of combterm * combterm 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

42 

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

43 
datatype locality = General  Intro  Elim  Simp  Local  Assum  Chained 
42613
23b13b1bd565
use strings to encode type systems in ATP module, to reduce the amount of outofplace information and also to make it easier to print the type system used
blanchet
parents:
42612
diff
changeset

44 

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

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

46 
datatype type_level = 
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

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

49 

43102  50 
datatype type_sys = 
42722  51 
Simple_Types of type_level  
42837  52 
Preds of polymorphism * type_level * type_heaviness  
53 
Tags of polymorphism * type_level * type_heaviness 

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

54 

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

56 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

79 
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

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

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

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

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

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

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

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

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

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

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

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

92 
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

93 
val proxify_const : string > (string * string) option 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

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

97 
val make_schematic_var : string * int > string 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

99 
val make_schematic_type_var : string * int > string 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

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

103 
val make_type_class : string > string 
43093  104 
val new_skolem_var_name_from_const : string > string 
105 
val num_type_args : theory > string > int 

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

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

107 
theory > string list > class list > class list * arity_clause list 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

109 
theory > class list > class list > class_rel_clause list 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

110 
val combtyp_of : combterm > typ 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

111 
val strip_combterm_comb : combterm > combterm * combterm list 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

112 
val atyps_of : typ > typ list 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

114 
theory > (string * typ) list > term > combterm * typ list 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

115 
val is_locality_global : locality > bool 
43102  116 
val type_sys_from_string : string > type_sys 
117 
val polymorphism_of_type_sys : type_sys > polymorphism 

118 
val level_of_type_sys : type_sys > type_level 

119 
val is_type_sys_virtually_sound : type_sys > bool 

120 
val is_type_sys_fairly_sound : type_sys > bool 

121 
val choose_format : format list > type_sys > format * type_sys 

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

122 
val raw_type_literals_for_types : typ list > type_literal list 
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43130
diff
changeset

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

124 
connective > ('a, 'b, 'c) formula list > ('a, 'b, 'c) formula 
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset

125 
val unmangled_const_name : string > string 
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

126 
val unmangled_const : string > string * string fo_term list 
41088  127 
val translate_atp_fact : 
43102  128 
Proof.context > format > type_sys > bool > (string * locality) * thm 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

129 
> translated_formula option * ((string * locality) * thm) 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

131 
val should_specialize_helper : type_sys > term > bool 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

132 
val tfree_classes_of_terms : term list > string list 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

133 
val tvar_classes_of_terms : term list > string list 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

134 
val type_consts_of_terms : theory > term list > string list 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39975
diff
changeset

135 
val prepare_atp_problem : 
43102  136 
Proof.context > format > formula_kind > formula_kind > type_sys 
43096  137 
> bool option > bool > bool > term list > term 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

138 
> (translated_formula option * ((string * 'a) * thm)) list 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42540
diff
changeset

139 
> string problem * string Symtab.table * int * int 
42881
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

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

141 
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

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

143 

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

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

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

146 

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

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

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

149 

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

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

151 

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

152 
(* FIXME: avoid *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

153 
fun union_all xss = fold (union (op =)) xss [] 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

154 

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

155 
(* experimental *) 
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

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

157 

42879  158 
fun useful_isabelle_info s = 
159 
if generate_useful_info then 

160 
SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])])) 

161 
else 

162 
NONE 

163 

164 
val intro_info = useful_isabelle_info "intro" 

165 
val elim_info = useful_isabelle_info "elim" 

166 
val simp_info = useful_isabelle_info "simp" 

167 

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

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

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

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

171 

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

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

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

174 

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

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

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

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

178 

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

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

180 
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

181 
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

182 

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

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

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

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

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

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

189 
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

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

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

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

193 

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

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

195 
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

196 
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

197 

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

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

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

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

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

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

203 

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

205 
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

206 
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

207 

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

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

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

210 

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

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

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

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

214 
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

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

217 

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

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

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

220 
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

221 

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

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

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

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

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

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

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

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

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

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

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

232 

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

233 
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

234 

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

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

236 

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

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

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

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

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

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

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

243 
(* Three types of _ escapes: __, _A to _P, _nnn *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

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

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

248 
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

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

250 
let val digits = List.take (c::cs, 3) handle Subscript => [] in 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

252 
SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2)) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

255 
 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

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

257 

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

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

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

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

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

262 
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

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

264 
NONE 
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 proxy_table = 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

279 
("equal", (@{const_name HOL.eq}, (@{thm fequal_def}, 
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43139
diff
changeset

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

281 

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

282 
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

283 

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

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

285 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

305 

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

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

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

308 
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

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

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

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

312 

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

313 
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

314 
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

315 

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

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

317 
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

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

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

320 

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

321 
(*Remove the initial ' character from a type variable, if it is present*) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

323 
if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

324 
else raise Fail ("trim_type: Malformed type variable encountered: " ^ s) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

325 

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

326 
fun ascii_of_indexname (v,0) = ascii_of v 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

327 
 ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

328 

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

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

330 
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

331 
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

332 

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

333 
fun make_schematic_type_var (x,i) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

334 
tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i)) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

335 
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

336 

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

337 
(* HOL.eq MUST BE "equal" because it's built into ATPs. *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

338 
fun make_fixed_const @{const_name HOL.eq} = "equal" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

340 

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

341 
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

342 

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

343 
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

344 

43093  345 
fun new_skolem_var_name_from_const s = 
346 
let val ss = s > space_explode Long_Name.separator in 

347 
nth ss (length ss  2) 

348 
end 

349 

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

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

352 
constant name. *) 

353 
fun num_type_args thy s = 

354 
if String.isPrefix skolem_const_prefix s then 

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

356 
else 

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

358 

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

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

360 

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

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

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

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

364 
TyLitFree of name * name 
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 

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

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

368 

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

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

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

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

372 

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

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

375 

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

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

377 
 pack_sort (tvar, "HOL.type" :: srt) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

378 
pack_sort (tvar, srt) (* IGNORE sort "type" *) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

379 
 pack_sort (tvar, cls :: srt) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

380 
(`make_type_class cls, `I tvar) :: pack_sort (tvar, srt) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

381 

43086  382 
type arity_clause = 
383 
{name: string, 

384 
prem_lits: arity_literal list, 

385 
concl_lits: arity_literal} 

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

386 

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

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

388 
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

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

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

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

392 
in 
43086  393 
{name = name, 
394 
prem_lits = map TVarLit (union_all (map pack_sort tvars_srts)), 

395 
concl_lits = TConsLit (`make_type_class cls, 

396 
`make_fixed_type_const tcons, 

397 
tvars ~~ tvars)} 

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

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

399 

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

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

401 
 arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

402 
arity_clause seen n (tcons,ars) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

403 
 arity_clause seen n (tcons, (ar as (class,_)) :: ars) = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

404 
if member (op =) seen class then (*multiple arities for the same tycon, class pair*) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

405 
make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) :: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

406 
arity_clause seen (n+1) (tcons,ars) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

408 
make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

409 
arity_clause (class::seen) n (tcons,ars) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

410 

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

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

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

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

414 

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

415 
(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

416 
provided its arguments have the corresponding sorts.*) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

421 
fun add_class tycon class = 

422 
cons (class, domain_sorts tycon class) 

423 
handle Sorts.CLASS_ERROR _ => I 

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

425 
in map try_classes tycons end 

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

426 

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

427 
(*Proving one (tycon, class) membership may require proving others, so iterate.*) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

429 
 iter_type_class_pairs thy tycons classes = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

430 
let val cpairs = type_class_pairs thy tycons classes 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

431 
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

432 
> subtract (op =) classes > subtract (op =) HOLogic.typeS 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

433 
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses 
43093  434 
in (union (op =) 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 = 
443 
{name: string, 

444 
subclass: name, 

445 
superclass: name} 

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

446 

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

447 
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

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

451 
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

452 
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

453 
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

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

455 

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

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

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 

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

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

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

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

467 
CombApp of combterm * combterm 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

468 

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

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

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

471 
 combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1)) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

472 

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

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

474 
fun strip_combterm_comb u = 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

475 
let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

478 

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

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

480 

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

481 
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

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

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

484 

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

485 
(* Converts a term (with combinators) into a combterm. Also accumulates sort 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

513 
> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T)) 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

514 
 combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

515 

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

516 
datatype locality = General  Intro  Elim  Simp  Local  Assum  Chained 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

517 

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

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

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

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

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

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

523 

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

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

525 
datatype type_level = 
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

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

528 

43102  529 
datatype type_sys = 
42722  530 
Simple_Types of type_level  
42837  531 
Preds of polymorphism * type_level * type_heaviness  
532 
Tags of polymorphism * type_level * type_heaviness 

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

533 

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

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

535 
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

536 

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

537 
fun type_sys_from_string s = 
42722  538 
(case try (unprefix "poly_") s of 
539 
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

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

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

544 
case try (unprefix "mangled_") s of 

545 
SOME s => (SOME Mangled_Monomorphic, s) 

546 
 NONE => (NONE, s)) 

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

547 
> (fn s => 
42689
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

548 
(* "_query" and "_bang" are for the ASCIIchallenged Mirabelle. *) 
e38590764c34
versions of ! and ? for the ASCIIchallenged Mirabelle
blanchet
parents:
42688
diff
changeset

549 
case try_unsuffixes ["?", "_query"] s of 
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

550 
SOME s => (Nonmonotonic_Types, s) 
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

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

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

553 
SOME s => (Finite_Types, s) 
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

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

42837  559 
> (fn (poly, (level, (heaviness, core))) => 
560 
case (core, (poly, level, heaviness)) of 

43128  561 
("simple", (NONE, _, Lightweight)) => Simple_Types level 
42854
d99167ac4f8a
since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents:
42852
diff
changeset

562 
 ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) 
42851
3bb63850488b
removed "poly_tags_light_bang" since highly unsound
blanchet
parents:
42837
diff
changeset

563 
 ("tags", (SOME Polymorphic, All_Types, _)) => 
42854
d99167ac4f8a
since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents:
42852
diff
changeset

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

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

566 
(* The actual light encoding is very unsound. *) 
43128  567 
Tags (Polymorphic, level, Heavyweight) 
42854
d99167ac4f8a
since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
blanchet
parents:
42852
diff
changeset

568 
 ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) 
43128  569 
 ("args", (SOME poly, All_Types (* naja *), Lightweight)) => 
570 
Preds (poly, Const_Arg_Types, Lightweight) 

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

572 
Preds (Polymorphic, No_Types, Lightweight) 

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

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

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

575 

42722  576 
fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic 
42828  577 
 polymorphism_of_type_sys (Preds (poly, _, _)) = poly 
578 
 polymorphism_of_type_sys (Tags (poly, _, _)) = poly 

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

579 

42722  580 
fun level_of_type_sys (Simple_Types level) = level 
42828  581 
 level_of_type_sys (Preds (_, level, _)) = level 
582 
 level_of_type_sys (Tags (_, level, _)) = level 

583 

43128  584 
fun heaviness_of_type_sys (Simple_Types _) = Heavyweight 
42837  585 
 heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness 
586 
 heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness 

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

587 

42687  588 
fun is_type_level_virtually_sound level = 
589 
level = All_Types orelse level = Nonmonotonic_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

590 
val is_type_sys_virtually_sound = 
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

591 
is_type_level_virtually_sound o level_of_type_sys 
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

592 

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

593 
fun is_type_level_fairly_sound level = 
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

594 
is_type_level_virtually_sound level orelse level = Finite_Types 
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

595 
val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys 
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

596 

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

597 
fun is_setting_higher_order THF (Simple_Types _) = true 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

598 
 is_setting_higher_order _ _ = false 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

599 

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

600 
fun choose_format formats (Simple_Types level) = 
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

601 
if member (op =) formats THF then (THF, Simple_Types level) 
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

602 
else if member (op =) formats TFF then (TFF, Simple_Types level) 
43128  603 
else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight)) 
43101
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

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

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

606 
CNF_UEQ => 
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

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

608 
Preds stuff => 
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

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

610 
stuff 
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

611 
 _ => type_sys) 
1d46d85cd78b
make "prepare_atp_problem" more robust w.r.t. choice of type system
blanchet
parents:
43098
diff
changeset

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

613 

40114  614 
type translated_formula = 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

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

616 
locality: locality, 
42525
7a506b0b644f
distinguish FOF and TFF (typed firstorder) in ATP abstract syntax tree
blanchet
parents:
42524
diff
changeset

617 
kind: formula_kind, 
42562  618 
combformula: (name, typ, combterm) formula, 
619 
atomic_types: typ list} 

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

620 

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

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

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

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

625 

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

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

627 

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

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

629 

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

630 
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

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

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

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

634 
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

635 

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

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

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

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

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

640 
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

641 

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

644 
 should_drop_arg_type_args type_sys = 

645 
level_of_type_sys type_sys = All_Types andalso 

43128  646 
heaviness_of_type_sys type_sys = Heavyweight 
42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

647 

43128  648 
fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args 
43105
bb0ceef7d39f
no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents:
43104
diff
changeset

649 
 general_type_arg_policy type_sys = 
bb0ceef7d39f
no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents:
43104
diff
changeset

650 
if level_of_type_sys type_sys = No_Types then 
bb0ceef7d39f
no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents:
43104
diff
changeset

651 
No_Type_Args 
bb0ceef7d39f
no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents:
43104
diff
changeset

652 
else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then 
bb0ceef7d39f
no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents:
43104
diff
changeset

653 
Mangled_Type_Args (should_drop_arg_type_args type_sys) 
bb0ceef7d39f
no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents:
43104
diff
changeset

654 
else 
bb0ceef7d39f
no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents:
43104
diff
changeset

655 
Explicit_Type_Args (should_drop_arg_type_args type_sys) 
42563  656 

42951
40bf0173fbed
pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents:
42944
diff
changeset

657 
fun type_arg_policy type_sys s = 
40bf0173fbed
pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents:
42944
diff
changeset

658 
if s = @{const_name HOL.eq} orelse 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

659 
(s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then 
42951
40bf0173fbed
pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents:
42944
diff
changeset

660 
No_Type_Args 
43105
bb0ceef7d39f
no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents:
43104
diff
changeset

661 
else if s = type_tag_name then 
bb0ceef7d39f
no need for type arguments with "xxx_tags_heavy" type system
blanchet
parents:
43104
diff
changeset

662 
Explicit_Type_Args false 
42951
40bf0173fbed
pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents:
42944
diff
changeset

663 
else 
40bf0173fbed
pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
blanchet
parents:
42944
diff
changeset

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

665 

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

666 
(*Make literals for sorted type variables*) 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

667 
fun generic_sorts_on_type (_, []) = [] 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

668 
 generic_sorts_on_type ((x, i), s :: ss) = 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

669 
generic_sorts_on_type ((x, i), ss) 
43093  670 
> (if s = the_single @{sort HOL.type} then 
671 
I 

672 
else if i = ~1 then 

673 
cons (TyLitFree (`make_type_class s, `make_fixed_type_var x)) 

674 
else 

675 
cons (TyLitVar (`make_type_class s, 

676 
(make_schematic_type_var (x, i), x)))) 

43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

677 
fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

678 
 sorts_on_tfree _ = [] 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

679 
fun sorts_on_tvar (TVar z) = generic_sorts_on_type z 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

680 
 sorts_on_tvar _ = [] 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

681 

43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

682 
(* Given a list of sorted type variables, return a list of type literals. *) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

683 
fun raw_type_literals_for_types Ts = 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

684 
union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

685 

e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

686 
fun type_literals_for_types type_sys sorts_on_typ Ts = 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

687 
if level_of_type_sys type_sys = No_Types then [] 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

688 
else union_all (map sorts_on_typ Ts) 
41137
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

689 

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

690 
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

691 
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

692 
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

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

694 
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

695 
 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

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

697 
 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

698 
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

699 
 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

700 

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

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

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

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

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

706 
 formula_vars bounds (AAtom tm) = 
42526  707 
union (op =) (atom_vars tm [] 
708 
> filter_out (member (op =) bounds o fst)) 

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

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

710 

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

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

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

715 

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

716 
fun term_vars (ATerm (name as (s, _), tms)) = 
42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

717 
is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms 
42674  718 
fun close_formula_universally phi = close_universally term_vars phi 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

719 

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

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

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

722 

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

723 
fun fo_term_from_typ format type_sys = 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

725 
fun term (Type (s, Ts)) = 
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

726 
ATerm (case (is_setting_higher_order format type_sys, s) of 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

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

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

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

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

732 
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

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

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

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

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

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

738 
in term end 
42562  739 

740 
(* This shouldn't clash with anything else. *) 

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

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

742 

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

745 
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

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

747 

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

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

749 

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

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

751 
if s = tptp_bool_type orelse s = tptp_fun_type orelse 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

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

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

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

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

756 

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

757 
fun ho_type_from_fo_term format type_sys pred_sym ary = 
42963  758 
let 
759 
fun to_atype ty = 

760 
AType ((make_simple_type (generic_mangled_type_name fst ty), 

761 
generic_mangled_type_name snd ty)) 

762 
fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) 

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

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

764 
 to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary  1)) tys 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

765 
fun to_ho (ty as ATerm ((s, _), tys)) = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

766 
if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty 
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

767 
in if is_setting_higher_order format type_sys then to_ho else to_fo ary end 
42963  768 

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

769 
fun mangled_type format type_sys pred_sym ary = 
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

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

771 
o fo_term_from_typ format type_sys 
42963  772 

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

773 
fun mangled_const_name format type_sys T_args (s, s') = 
42963  774 
let 
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

775 
val ty_args = map (fo_term_from_typ format type_sys) T_args 
42963  776 
fun type_suffix f g = 
777 
fold_rev (curry (op ^) o g o prefix mangled_type_sep 

778 
o generic_mangled_type_name f) ty_args "" 

779 
in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end 

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

780 

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

781 
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

782 
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

783 

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

784 
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

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

786 
 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

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

788 
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

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

790 

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

791 
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

792 
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

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

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

795 
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

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

797 

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

798 
val unmangled_const_name = space_explode mangled_type_sep #> hd 
42542
024920b65ce2
perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
blanchet
parents:
42541
diff
changeset

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

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

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

802 
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

803 

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

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

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

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

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

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

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

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

811 
if top_level orelse is_setting_higher_order format type_sys then 
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

823 
else 
42574  824 
(proxy_base >> prefix const_prefix, T_args) 
825 
 NONE => (name, T_args)) 

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

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

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

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

829 

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

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

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

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

833 
combterm_from_term thy bs (Envir.eta_contract t) 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

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

836 
fun do_quant bs q s T t' = 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

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

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

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

841 
and do_conn bs c t1 t2 = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

842 
do_formula bs t1 ##>> do_formula bs t2 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42530
diff
changeset

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

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

845 
case t of 
43096  846 
@{const Trueprop} $ t1 => do_formula bs t1 
847 
 @{const Not} $ t1 => do_formula bs t1 #>> mk_anot 

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

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

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

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

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

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

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

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

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

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

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

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

859 

42750
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

860 
fun presimplify_term ctxt = 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

861 
Skip_Proof.make_thm (Proof_Context.theory_of ctxt) 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

862 
#> Meson.presimplify ctxt 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

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

864 

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

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

867 
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

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

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

870 
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

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

872 

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

873 
fun extensionalize_term ctxt t = 
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

874 
let val thy = Proof_Context.theory_of ctxt in 
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

875 
t > cterm_of thy > Meson.extensionalize_conv ctxt 
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

876 
> prop_of > Logic.dest_equals > snd 
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

877 
end 
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

878 

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

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

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

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

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

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

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

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

887 
@{const Not} $ t1 => @{const Not} $ aux Ts t1 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

888 
 (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

889 
t0 $ Abs (s, T, aux (T :: Ts) t') 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

890 
 (t0 as Const (@{const_name All}, _)) $ t1 => 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

891 
aux Ts (t0 $ eta_expand Ts t1 1) 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

892 
 (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

893 
t0 $ Abs (s, T, aux (T :: Ts) t') 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

894 
 (t0 as Const (@{const_name Ex}, _)) $ t1 => 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

895 
aux Ts (t0 $ eta_expand Ts t1 1) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

896 
 (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

897 
 (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

898 
 (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

899 
 (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

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

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

902 
 _ => if not (exists_subterm (fn Abs _ => true  _ => false) t) then 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

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

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

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

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

907 
> cterm_of thy 
39890  908 
> Meson_Clausify.introduce_combinators_in_cterm 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

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

910 
> reveal_bounds Ts 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39005
diff
changeset

911 
val (t, ctxt') = Variable.import_terms true [t] ctxt >> the_single 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

912 
in t > aux [] > singleton (Variable.export_terms ctxt' ctxt) end 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

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

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

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

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

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

918 

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

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

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

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

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

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

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

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

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

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

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

929 

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

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

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

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

935 
> Object_Logic.atomize_term thy 
42563  936 
val need_trueprop = (fastype_of t = @{typ bool}) 
43096  937 
in 
938 
t > need_trueprop ? HOLogic.mk_Trueprop 

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

940 
> extensionalize_term ctxt 

941 
> presimp ? presimplify_term ctxt 

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

942 
> perhaps (try (HOLogic.dest_Trueprop)) 
43096  943 
> introduce_combinators_in_term ctxt kind 
944 
end 

945 

946 
(* making fact and conjecture formulas *) 

947 
fun make_formula thy format type_sys eq_as_iff name loc kind t = 

948 
let 

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

949 
val (combformula, atomic_types) = 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

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

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

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

955 

43096  956 
fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

957 
((name, loc), t) = 
43096  958 
let val thy = Proof_Context.theory_of ctxt in 
959 
case (keep_trivial, 

960 
t > preproc ? preprocess_prop ctxt presimp Axiom 

961 
> make_formula thy format type_sys eq_as_iff name loc Axiom) of 

962 
(false, 

963 
formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) => 

964 
if s = tptp_true then NONE else SOME formula 

965 
 (_, formula) => SOME formula 

966 
end 

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

967 

43096  968 
fun make_conjecture ctxt format prem_kind type_sys preproc ts = 
969 
let 

970 
val thy = Proof_Context.theory_of ctxt 

971 
val last = length ts  1 

972 
in 

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

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

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

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

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

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

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

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

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

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

982 
in 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

983 
t > preproc ? (preprocess_prop ctxt true kind #> freeze_term) 
43096  984 
> make_formula thy format type_sys true (string_of_int j) 
985 
General kind 

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

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

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

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

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

990 

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

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

992 

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

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

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

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

996 

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

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

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

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

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

1001 

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

1002 
fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T = 
208ec29cc013
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
blanchet
parents:
42885
diff
changeset

1003 
exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts 
42836  1004 
 should_encode_type _ _ All_Types _ = true 
42682
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

1005 
 should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T 
562046fd8e0c
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFFtypes)
blanchet
parents:
42680
diff
changeset

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

1007 

42837  1008 
fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness)) 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

1009 
should_predicate_on_var T = 
43128  1010 
(heaviness = Heavyweight orelse should_predicate_on_var ()) andalso 
42878
85ac4c12a4b7
slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
blanchet
parents:
42855
diff
changeset

1011 
should_encode_type ctxt nonmono_Ts level T 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

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

1013 

42836  1014 
fun is_var_or_bound_var (CombConst ((s, _), _, _)) = 
1015 
String.isPrefix bound_var_prefix s 

1016 
 is_var_or_bound_var (CombVar _) = true 

1017 
 is_var_or_bound_var _ = false 

1018 

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

1019 
datatype tag_site = Top_Level  Eq_Arg  Elsewhere 
1558741f8a72
started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents:
42828
diff
changeset

1020 

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

1021 
fun should_tag_with_type _ _ _ Top_Level _ _ = false 
42837  1022 
 should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T = 
1023 
(case heaviness of 

43128  1024 
Heavyweight => should_encode_type ctxt nonmono_Ts level T 
1025 
 Lightweight => 

42836  1026 
case (site, is_var_or_bound_var u) of 
1027 
(Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T 

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

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

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

1030 

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

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

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

1033 
val should_encode = should_encode_type ctxt nonmono_Ts level 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1034 
fun homo 0 T = if should_encode T then T else homo_infinite_type 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1035 
 homo ary (Type (@{type_name fun}, [T1, T2])) = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

1036 
homo 0 T1 > homo (ary  1) T2 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

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

1039 

42573
744215c3e90c
got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
blanchet
parents:
42572
diff
changeset

1040 
(** "hBOOL" and "hAPP" **) 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

1041 

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

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

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

1045 
fun add_combterm_syms_to_table ctxt explicit_apply = 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

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

1047 
fun consider_var_arity const_T var_T max_ary = 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

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

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

1050 
if ary = max_ary orelse type_instance ctxt (var_T, T) then ary 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1051 
else iter (ary + 1) (range_type T) 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

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

1053 
fun add top_level tm (accum as (ho_var_Ts, sym_tab)) = 
43167
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1054 
let 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1055 
fun do_var_or_bound_var T = 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1056 
if explicit_apply = NONE andalso can dest_funT T then 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1057 
let 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1058 
fun repair_min_arity {pred_sym, min_ary, max_ary, types} = 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1059 
{pred_sym = pred_sym, 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1060 
min_ary = 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1061 
fold (fn T' => consider_var_arity T' T) types min_ary, 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1062 
max_ary = max_ary, types = types} 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1063 
val ho_var_Ts' = ho_var_Ts > insert_type ctxt I T 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1064 
in 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1065 
if pointer_eq (ho_var_Ts', ho_var_Ts) then accum 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1066 
else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab) 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1067 
end 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1068 
else 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1069 
accum 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1070 
val (head, args) = strip_combterm_comb tm 
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1071 
in 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

1072 
(case head of 
42563  1073 
CombConst ((s, _), T, _) => 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

1074 
if String.isPrefix bound_var_prefix s then 
43167
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1075 
do_var_or_bound_var T 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

1076 
else 
43139
9ed5d8ad8fa0
fixed debilitating translation bug introduced in b6e61d22fa61  "equal" and "=" should always have arity 2
blanchet
parents:
43136
diff
changeset

1077 
let val ary = length args in 
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

1078 
(ho_var_Ts, 
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

1079 
case Symtab.lookup sym_tab s of 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1080 
SOME {pred_sym, min_ary, max_ary, types} => 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

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

1082 
val types' = types > insert_type ctxt I T 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

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

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

1085 
pointer_eq (types', types) then 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

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

1087 
else 
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

1088 
fold (consider_var_arity T) ho_var_Ts min_ary 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

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

1090 
Symtab.update (s, {pred_sym = pred_sym andalso top_level, 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1091 
min_ary = Int.min (ary, min_ary), 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1092 
max_ary = Int.max (ary, max_ary), 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

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

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

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

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

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

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

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

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

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

1102 
 NONE => fold (consider_var_arity T) ho_var_Ts ary 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

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

1104 
Symtab.update_new (s, {pred_sym = top_level, 
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

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

1106 
types = [T]}) 
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

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

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

1109 
end 
43167
839f599bc7ed
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
blanchet
parents:
43159
diff
changeset

1110 
 CombVar (_, T) => do_var_or_bound_var T 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43039
diff
changeset

1111 
 _ => accum) 
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

1112 
> fold (add false) args 
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

1113 
end 
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

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

1115 
fun add_fact_syms_to_table ctxt explicit_apply = 
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

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

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

1118 

43139
9ed5d8ad8fa0
fixed debilitating translation bug introduced in b6e61d22fa61  "equal" and "=" should always have arity 2
blanchet
parents:
43136
diff
changeset

1119 
val default_sym_tab_entries : (string * sym_info) list = 
43174  1120 
(prefixed_predicator_name, 
43139
9ed5d8ad8fa0
fixed debilitating translation bug introduced in b6e61d22fa61  "equal" and "=" should always have arity 2
blanchet
parents:
43136
diff
changeset

1121 
{pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

1122 
([tptp_false, tptp_true] 
43139
9ed5d8ad8fa0
fixed debilitating translation bug introduced in b6e61d22fa61  "equal" and "=" should always have arity 2
blanchet
parents:
43136
diff
changeset

1123 
> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ 
9ed5d8ad8fa0
fixed debilitating translation bug introduced in b6e61d22fa61  "equal" and "=" should always have arity 2
blanchet
parents:
43136
diff
changeset

1124 
([tptp_equal, tptp_old_equal] 
9ed5d8ad8fa0
fixed debilitating translation bug introduced in b6e61d22fa61  "equal" and "=" should always have arity 2
blanchet
parents:
43136
diff
changeset

1125 
> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []})) 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

1126 

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

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

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

1129 
> pair [] > fold (add_fact_syms_to_table ctxt explicit_apply) facts > snd 
43139
9ed5d8ad8fa0
fixed debilitating translation bug introduced in b6e61d22fa61  "equal" and "=" should always have arity 2
blanchet
parents:
43136
diff
changeset

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

1131 

42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

1132 
fun min_arity_of sym_tab s = 
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

1133 
case Symtab.lookup sym_tab s of 
42574  1134 
SOME ({min_ary, ...} : sym_info) => min_ary 
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

1135 
 NONE => 
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

1136 
case strip_prefix_and_unascii const_prefix s of 
42547
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

1137 
SOME s => 
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

1138 
let val s = s > unmangled_const_name > invert_const in 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

1139 
if s = predicator_name then 1 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

1140 
else if s = app_op_name then 2 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

1141 
else if s = type_pred_name then 1 
42557
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

1142 
else 0 
42547
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

1143 
end 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, wh 