author  blanchet 
Mon, 30 May 2011 17:00:38 +0200  
changeset 43064  b6e61d22fa61 
parent 43039  b967219cec78 
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 

40068  9 
signature SLEDGEHAMMER_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 
42939  12 
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

13 
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

14 
type 'a problem = 'a ATP_Problem.problem 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

15 
type locality = Sledgehammer_Filter.locality 
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

16 

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

17 
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

18 
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

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

21 

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

22 
datatype type_system = 
42722  23 
Simple_Types of type_level  
42837  24 
Preds of polymorphism * type_level * type_heaviness  
25 
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

26 

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

28 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42645
diff
changeset

29 
val readable_names : bool Config.T 
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

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

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

32 
val helper_prefix : string 
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

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

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

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

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

37 
val simple_type_prefix : string 
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

38 
val type_sys_from_string : string > type_system 
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

39 
val polymorphism_of_type_sys : type_system > polymorphism 
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

40 
val level_of_type_sys : type_system > 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

41 
val is_type_sys_virtually_sound : type_system > bool 
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

42 
val is_type_sys_fairly_sound : type_system > bool 
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

43 
val unmangled_const : string > string * string fo_term list 
41088  44 
val translate_atp_fact : 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

45 
Proof.context > format > type_system > bool > (string * locality) * thm 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

46 
> translated_formula option * ((string * locality) * thm) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39975
diff
changeset

47 
val prepare_atp_problem : 
42939  48 
Proof.context > format > formula_kind > formula_kind > type_system 
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

49 
> bool option > term list > term 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

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

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

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

53 
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

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

55 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

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

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

58 

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

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

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

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

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

63 

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

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

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

66 

42879  67 
fun useful_isabelle_info s = 
68 
if generate_useful_info then 

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

70 
else 

71 
NONE 

72 

73 
val intro_info = useful_isabelle_info "intro" 

74 
val elim_info = useful_isabelle_info "elim" 

75 
val simp_info = useful_isabelle_info "simp" 

76 

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

77 
(* Readable names are often much shorter, especially if types are mangled in 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

78 
names. Also, the logic for generating legal SNARK sort names is only 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

79 
implemented for readable names. Finally, readable names are, well, more 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

80 
readable. For these reason, they are enabled by default. *) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42645
diff
changeset

81 
val readable_names = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42645
diff
changeset

82 
Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

83 

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

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

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

86 
val sym_formula_prefix = "sym_" 
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

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

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

89 
val helper_prefix = "help_" 
42543
f9d402d144d4
declare TFF types so that SNARK can be used with types
blanchet
parents:
42542
diff
changeset

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

91 
val arity_clause_prefix = "arity_" 
39975
7c50d5ca5c04
avoid generating several formulas with the same name ("tfrees")
blanchet
parents:
39954
diff
changeset

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

93 

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

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

95 
val untyped_helper_suffix = "_U" 
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

96 

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

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

98 
val app_op_name = "hAPP" 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

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

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

101 

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

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

103 
if s = tptp_bool_type orelse s = tptp_fun_type orelse 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

104 
s = tptp_individual_type then 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

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

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

108 

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

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

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

111 

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

112 
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

113 
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

114 
All_Types  Nonmonotonic_Types  Finite_Types  Const_Arg_Types  No_Types 
42837  115 
datatype type_heaviness = Heavy  Light 
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

116 

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

117 
datatype type_system = 
42722  118 
Simple_Types of type_level  
42837  119 
Preds of polymorphism * type_level * type_heaviness  
120 
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

121 

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

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

123 
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

124 

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

125 
fun type_sys_from_string s = 
42722  126 
(case try (unprefix "poly_") s of 
127 
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

128 
 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

129 
case try (unprefix "mono_") s of 
42722  130 
SOME s => (SOME Monomorphic, s) 
131 
 NONE => 

132 
case try (unprefix "mangled_") s of 

133 
SOME s => (SOME Mangled_Monomorphic, s) 

134 
 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

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

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

137 
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

138 
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

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

140 
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

141 
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

142 
 NONE => (All_Types, s)) 
42828  143 
> apsnd (fn s => 
42837  144 
case try (unsuffix "_heavy") s of 
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

145 
SOME s => (Heavy, s) 
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

146 
 NONE => (Light, s)) 
42837  147 
> (fn (poly, (level, (heaviness, core))) => 
148 
case (core, (poly, level, heaviness)) of 

42855  149 
("simple", (NONE, _, Light)) => 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

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

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

152 
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

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

154 
(* The actual light encoding is very unsound. *) 
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

155 
Tags (Polymorphic, level, Heavy) 
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

156 
 ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) 
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

157 
 ("args", (SOME poly, All_Types (* naja *), Light)) => 
42837  158 
Preds (poly, Const_Arg_Types, Light) 
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

159 
 ("erased", (NONE, All_Types (* naja *), Light)) => 
42837  160 
Preds (Polymorphic, No_Types, Light) 
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

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

162 
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

163 

42722  164 
fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic 
42828  165 
 polymorphism_of_type_sys (Preds (poly, _, _)) = poly 
166 
 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

167 

42722  168 
fun level_of_type_sys (Simple_Types level) = level 
42828  169 
 level_of_type_sys (Preds (_, level, _)) = level 
170 
 level_of_type_sys (Tags (_, level, _)) = level 

171 

42837  172 
fun heaviness_of_type_sys (Simple_Types _) = Heavy 
173 
 heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness 

174 
 heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness 

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

175 

42687  176 
fun is_type_level_virtually_sound level = 
177 
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

178 
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

179 
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

180 

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

181 
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

182 
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

183 
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

184 

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

185 
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

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

187 

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

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

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

191 
kind: formula_kind, 
42562  192 
combformula: (name, typ, combterm) formula, 
193 
atomic_types: typ list} 

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

194 

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

195 
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

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

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

199 

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

200 
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

201 

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

202 
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

203 

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

204 
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

205 
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

206 
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

207 
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

208 
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

209 

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

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

211 
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

212 
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

213 
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

214 
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

215 

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

218 
 should_drop_arg_type_args type_sys = 

219 
level_of_type_sys type_sys = All_Types andalso 

42837  220 
heaviness_of_type_sys type_sys = Heavy 
42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

221 

42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

222 
fun general_type_arg_policy type_sys = 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

223 
if level_of_type_sys type_sys = No_Types then 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

224 
No_Type_Args 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

225 
else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then 
42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

226 
Mangled_Type_Args (should_drop_arg_type_args type_sys) 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

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

228 
Explicit_Type_Args (should_drop_arg_type_args type_sys) 
42563  229 

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

230 
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

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

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

233 
No_Type_Args 
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

234 
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

235 
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

236 

42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

237 
fun atp_type_literals_for_types format type_sys kind Ts = 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

238 
if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then 
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

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

240 
else 
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

241 
Ts > type_literals_for_types 
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

242 
> filter (fn TyLitVar _ => kind <> Conjecture 
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

243 
 TyLitFree _ => kind = Conjecture) 
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

244 

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

245 
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

246 
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

247 
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

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

249 
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

250 
 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

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

252 
 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

253 
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

254 
 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

255 

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

256 
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

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

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

260 
 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

261 
 formula_vars bounds (AAtom tm) = 
42526  262 
union (op =) (atom_vars tm [] 
263 
> 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

264 
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

265 

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

266 
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

267 
 combterm_vars (CombConst _) = I 
42574  268 
 combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) 
42674  269 
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

270 

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

271 
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

272 
is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms 
42674  273 
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

274 

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

275 
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

276 
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

277 

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

278 
fun fo_term_from_typ higher_order = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

280 
fun term (Type (s, Ts)) = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

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

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

284 
 _ => if s = homo_infinite_type_name then `I tptp_individual_type 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

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

287 
 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

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

289 
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

290 
in term end 
42562  291 

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

293 
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

294 

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

297 
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

298 
^ ")" 
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

299 

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

300 
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

301 

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

302 
fun ho_type_from_fo_term higher_order pred_sym ary = 
42963  303 
let 
304 
fun to_atype ty = 

305 
AType ((make_simple_type (generic_mangled_type_name fst ty), 

306 
generic_mangled_type_name snd ty)) 

307 
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

308 
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

309 
 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

310 
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

311 
if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

312 
in if higher_order then to_ho else to_fo ary end 
42963  313 

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

314 
fun mangled_type higher_order pred_sym ary = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

315 
ho_type_from_fo_term higher_order pred_sym ary o fo_term_from_typ higher_order 
42963  316 

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

317 
fun mangled_const_name T_args (s, s') = 
42963  318 
let 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

319 
val ty_args = map (fo_term_from_typ false) T_args 
42963  320 
fun type_suffix f g = 
321 
fold_rev (curry (op ^) o g o prefix mangled_type_sep 

322 
o generic_mangled_type_name f) ty_args "" 

323 
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

324 

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

325 
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

326 
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

327 

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

328 
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

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

330 
 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

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

332 
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

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

334 

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

335 
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

336 
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

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

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

339 
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

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

341 

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

342 
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

343 
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

344 
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

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

346 
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

347 

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

348 
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

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

350 
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

351 
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

352 
 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

353 
(case proxify_const s of 
43017
944b19ab6003
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
blanchet
parents:
43001
diff
changeset

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

355 
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

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

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

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

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

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

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

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

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

364 
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

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

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

367 
else 
42574  368 
(proxy_base >> prefix const_prefix, T_args) 
369 
 NONE => (name, T_args)) 

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

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

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

373 

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

374 
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

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

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

377 
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

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

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

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

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

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

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

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

386 
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

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

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

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

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

391 
 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

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

393 
 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

394 
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

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

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

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

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

399 
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

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

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

402 

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

403 
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

404 
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

405 
#> 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

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

407 

41491  408 
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

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

410 
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

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

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

413 
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

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

415 

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

416 
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

417 
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

418 
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

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

420 
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

421 

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

422 
fun introduce_combinators_in_term ctxt kind t = 
42361  423 
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

424 
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

425 
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

426 
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

427 
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

428 
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

429 
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

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

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

432 
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

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

434 
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

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

436 
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

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

438 
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

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

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

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

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

443 
$ 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

444 
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

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

446 
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

447 
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

448 
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

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

450 
> cterm_of thy 
39890  451 
> 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

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

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

454 
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

455 
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

456 
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

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

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

459 
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

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

461 

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

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

463 
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

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

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

466 
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

467 
 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

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

469 
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

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

471 
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

472 

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

473 
(* making fact and conjecture formulas *) 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

474 
fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

475 
let 
42361  476 
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

477 
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

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

479 
> Object_Logic.atomize_term thy 
42563  480 
val need_trueprop = (fastype_of t = @{typ bool}) 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

481 
val t = t > need_trueprop ? HOLogic.mk_Trueprop 
42742
369dfc819056
unfold set constants in Sledgehammer/ATP as well if Metis does it too
blanchet
parents:
42734
diff
changeset

482 
> Raw_Simplifier.rewrite_term thy 
369dfc819056
unfold set constants in Sledgehammer/ATP as well if Metis does it too
blanchet
parents:
42734
diff
changeset

483 
(Meson.unfold_set_const_simps ctxt) [] 
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

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

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

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

487 
> introduce_combinators_in_term ctxt kind 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

488 
> kind <> Axiom ? freeze_term 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

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

490 
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

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

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

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

495 

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

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

497 
((name, loc), t) = 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

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

499 
make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of 
43001  500 
(false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) => 
501 
if s = tptp_true then NONE else SOME formula 

41990
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

502 
 (_, formula) => SOME formula 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42560
diff
changeset

503 

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

504 
fun make_conjecture ctxt format prem_kind type_sys ts = 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

505 
let val last = length ts  1 in 
42709
e7af132d48fe
allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents:
42701
diff
changeset

506 
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

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

508 
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

509 
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

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

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

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

513 
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

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

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

516 
t > make_formula ctxt format type_sys true true 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

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

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

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

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

522 

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

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

524 

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

525 
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

526 
 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

527 
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

528 

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

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

530 
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

531 
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

532 
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

533 

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

534 
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

535 
exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts 
42836  536 
 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

537 
 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

538 
 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

539 

42837  540 
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

541 
should_predicate_on_var T = 
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

542 
(heaviness = Heavy orelse should_predicate_on_var ()) andalso 
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

543 
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

544 
 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

545 

42836  546 
fun is_var_or_bound_var (CombConst ((s, _), _, _)) = 
547 
String.isPrefix bound_var_prefix s 

548 
 is_var_or_bound_var (CombVar _) = true 

549 
 is_var_or_bound_var _ = false 

550 

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

551 
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

552 

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

553 
fun should_tag_with_type _ _ _ Top_Level _ _ = false 
42837  554 
 should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T = 
555 
(case heaviness of 

556 
Heavy => should_encode_type ctxt nonmono_Ts level T 

557 
 Light => 

42836  558 
case (site, is_var_or_bound_var u) of 
559 
(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

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

561 
 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

562 

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

563 
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

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

565 
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

566 
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

567 
 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

568 
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

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

570 
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

571 

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

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

573 

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

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

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

577 
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

578 
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

579 
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

580 
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

581 
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

582 
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

583 
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

584 
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

585 
fun add top_level tm (accum as (ho_var_Ts, sym_tab)) = 
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

586 
let val (head, args) = strip_combterm_comb tm in 
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

587 
(case head of 
42563  588 
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

589 
if String.isPrefix bound_var_prefix s then 
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

590 
if explicit_apply = NONE andalso can dest_funT T 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

591 
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

592 
fun repair_min_arity {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

593 
{pred_sym = pred_sym, 
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

594 
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

595 
fold (fn T' => consider_var_arity T' T) types 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

596 
max_ary = max_ary, 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

597 
val ho_var_Ts' = ho_var_Ts > 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

598 
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

599 
if pointer_eq (ho_var_Ts', ho_var_Ts) then 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

600 
else (ho_var_Ts', Symtab.map (K repair_min_arity) 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

601 
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

602 
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

603 
accum 
42558
3d9930cb6770
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
blanchet
parents:
42557
diff
changeset

604 
else 
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

605 
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

606 
val ary = length args 
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

607 
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

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

609 
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

610 
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

611 
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

612 
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

613 
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

614 
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

615 
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

616 
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

617 
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

618 
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

619 
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

620 
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

621 
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

622 
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

623 
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

624 
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

625 
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

626 
 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

627 
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

628 
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

629 
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

630 
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

631 
 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

632 
 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

633 
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

634 
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

635 
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

636 
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

637 
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

638 
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

639 
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

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

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

642 
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

643 
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

644 
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

645 
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

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

647 

42675  648 
val default_sym_table_entries : (string * sym_info) list = 
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

649 
[(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, 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

650 
(tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}), 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

651 
(make_fixed_const predicator_name, 
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

652 
{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

653 
([tptp_false, tptp_true] 
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

654 
> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

655 

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

656 
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

657 
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

658 
> fold Symtab.default default_sym_table_entries 
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

659 
> pair [] > fold (add_fact_syms_to_table ctxt explicit_apply) facts > snd 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

660 

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

661 
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

662 
case Symtab.lookup sym_tab s of 
42574  663 
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

664 
 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

665 
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

666 
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

667 
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

668 
if s = predicator_name then 1 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

669 
else if s = app_op_name then 2 
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

670 
else if s = type_pred_name then 1 
42557
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

671 
else 0 
42547
b5eec0c99528
fixed arity of special constants if "explicit_apply" is set
blanchet
parents:
42546
diff
changeset

672 
end 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

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

674 

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

675 
(* True if the constant ever appears outside of the toplevel position in 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

676 
literals, or if it appears with different arities (e.g., because of different 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

677 
type instantiations). If false, the constant always receives all of its 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

678 
arguments and is used as a predicate. *) 
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

679 
fun is_pred_sym 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

680 
case Symtab.lookup sym_tab s of 
42574  681 
SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => 
682 
pred_sym andalso min_ary = max_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

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

684 

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

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

686 
CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, []) 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

687 
fun predicator tm = CombApp (predicator_combconst, tm) 
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

688 

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

689 
fun introduce_predicators_in_combterm sym_tab tm = 
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

690 
case strip_combterm_comb tm of 
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

691 
(CombConst ((s, _), _, _), _) => 
42568
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

692 
if is_pred_sym sym_tab s then tm else predicator tm 
7b9801a34836
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
blanchet
parents:
42566
diff
changeset

693 
 _ => predicator tm 
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

694 

42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

695 
fun list_app head args = fold (curry (CombApp o swap)) args head 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

696 

75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

697 
fun explicit_app arg head = 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

698 
let 
42562  699 
val head_T = combtyp_of head 
42693
3c2baf9b3c61
reverted 6efda6167e5d because unsound  Vampire found a counterexample
blanchet
parents:
42691
diff
changeset

700 
val (arg_T, res_T) = dest_funT head_T 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

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

702 
CombConst (`make_fixed_const app_op_name, head_T > head_T, 
42693
3c2baf9b3c61
reverted 6efda6167e5d because unsound  Vampire found a counterexample
blanchet
parents:
42691
diff
changeset

703 
[arg_T, res_T]) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

704 
in list_app explicit_app [head, arg] end 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

705 
fun list_explicit_app head args = fold explicit_app args head 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

706 

42565
93f58e6a6f3e
proper handling of partially applied proxy symbols
blanchet
parents:
42564
diff
changeset

707 
fun introduce_explicit_apps_in_combterm sym_tab = 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

708 
let 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

709 
fun aux tm = 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

710 
case strip_combterm_comb tm of 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

711 
(head as CombConst ((s, _), _, _), args) => 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

712 
args > map aux 
42557
ae0deb39a254
fixed minarity computation when "explicit_apply" is specified
blanchet
parents:
42556
diff
changeset

713 
> chop (min_arity_of sym_tab s) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

714 
>> list_app head 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

715 
> list_explicit_app 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

716 
 (head, args) => list_explicit_app head (map aux args) 
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

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

718 

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

719 
fun chop_fun 0 T = ([], T) 
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

720 
 chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = 
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

721 
chop_fun (n  1) ran_T >> cons dom_T 
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

722 
 chop_fun _ _ = raise Fail "unexpected nonfunction" 
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

723 

42780
be6164bc9744
avoid "UnequalLengths" exception for special constant "fequal"  and optimize code in the common case where no type arguments are needed
blanchet
parents:
42778
diff
changeset

724 
fun filter_type_args _ _ _ [] = [] 
be6164bc9744
avoid "UnequalLengths" exception for special constant "fequal"  and optimize code in the common case where no type arguments are needed
blanchet
parents:
42778
diff
changeset

725 
 filter_type_args thy s arity T_args = 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

726 
let 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

727 
(* will throw "TYPE" for pseudoconstants *) 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

728 
val U = if s = app_op_name then 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

729 
@{typ "('a => 'b) => 'a => 'b"} > Logic.varifyT_global 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

730 
else 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

731 
s > Sign.the_const_type thy 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

732 
in 
42781  733 
case Term.add_tvarsT (U > chop_fun arity > snd) [] of 
734 
[] => [] 

735 
 res_U_vars => 

736 
let val U_args = (s, U) > Sign.const_typargs thy in 

737 
U_args ~~ T_args 

738 
> map_filter (fn (U, T) => 

739 
if member (op =) res_U_vars (dest_TVar U) then 

740 
SOME T 

741 
else 

742 
NONE) 

743 
end 

42780
be6164bc9744
avoid "UnequalLengths" exception for special constant "fequal"  and optimize code in the common case where no type arguments are needed
blanchet
parents:
42778
diff
changeset

744 
end 
be6164bc9744
avoid "UnequalLengths" exception for special constant "fequal"  and optimize code in the common case where no type arguments are needed
blanchet
parents:
42778
diff
changeset

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

746 

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

747 
fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys = 
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

748 
let 
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

749 
val thy = Proof_Context.theory_of ctxt 
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

750 
fun aux arity (CombApp (tm1, tm2)) = 
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

751 
CombApp (aux (arity + 1) tm1, aux 0 tm2) 
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

752 
 aux arity (CombConst (name as (s, _), T, T_args)) = 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

753 
let 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

754 
val level = level_of_type_sys type_sys 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

755 
val (T, T_args) = 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

756 
(* Aggressively merge most "hAPPs" if the type system is unsound 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

757 
anyway, by distinguishing overloads only on the homogenized 
42837  758 
result type. Don't do it for lightweight type systems, though, 
759 
since it leads to too many unsound proofs. *) 

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

760 
if s = const_prefix ^ app_op_name andalso 
42726
70fc448a1815
avoid "Empty" exception by making sure that a certain optimization only is attempted when it makes sense
blanchet
parents:
42722
diff
changeset

761 
length T_args = 2 andalso 
42836  762 
not (is_type_sys_virtually_sound type_sys) andalso 
42837  763 
heaviness_of_type_sys type_sys = Heavy then 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

764 
T_args > map (homogenized_type ctxt nonmono_Ts level 0) 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

765 
> (fn Ts => let val T = hd Ts > nth Ts 1 in 
42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

766 
(T > T, tl Ts) 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

767 
end) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

768 
else 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

769 
(T, T_args) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

770 
in 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

771 
(case strip_prefix_and_unascii const_prefix s of 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

772 
NONE => (name, T_args) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

773 
 SOME s'' => 
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

774 
let 
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

775 
val s'' = invert_const s'' 
42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

776 
fun filtered_T_args false = T_args 
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

777 
 filtered_T_args true = filter_type_args thy s'' arity T_args 
42753
c9552e617acc
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
blanchet
parents:
42750
diff
changeset

778 
in 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

779 
case type_arg_policy type_sys s'' of 
42831
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

780 
Explicit_Type_Args drop_args => 
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

781 
(name, filtered_T_args drop_args) 
c9b0968484fb
more work on "shallow" encoding + adjustments to other encodings
blanchet
parents:
42830
diff
changeset

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

783 
(mangled_const_name (filtered_T_args drop_args) name, []) 
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

784 
 No_Type_Args => (name, []) 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

785 
end) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

786 
> (fn (name, T_args) => CombConst (name, T, T_args)) 
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

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

788 
 aux _ tm = tm 
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

789 
in aux 0 end 
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

790 

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

791 
fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab = 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

792 
not (is_setting_higher_order format type_sys) 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

793 
? (introduce_explicit_apps_in_combterm sym_tab 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

794 
#> introduce_predicators_in_combterm sym_tab) 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

795 
#> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

796 
fun repair_fact ctxt format nonmono_Ts type_sys sym_tab = 
42701
500e4a88675e
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
blanchet
parents:
42700
diff
changeset

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

798 
(repair_combterm ctxt format nonmono_Ts type_sys sym_tab)) 
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

799 

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

800 
(** Helper facts **) 
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

801 

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

802 
fun ti_ti_helper_fact () = 
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

803 
let 
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

804 
fun var s = ATerm (`I s, []) 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

805 
fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm]) 
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

806 
in 
42612  807 
Formula (helper_prefix ^ "ti_ti", Axiom, 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

808 
AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")])) 
42879  809 
> close_formula_universally, simp_info, NONE) 
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

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

811 

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

812 
fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) = 
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

813 
case strip_prefix_and_unascii const_prefix s of 
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

814 
SOME mangled_s => 
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

815 
let 
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

816 
val thy = Proof_Context.theory_of ctxt 
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

817 
val unmangled_s = mangled_s > unmangled_const_name 
42893
fd4babefe3f2
prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents:
42886
diff
changeset

818 
fun dub_and_inst c needs_fairly_sound (th, j) = 
42881
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

819 
((c ^ "_" ^ string_of_int j ^ 
42893
fd4babefe3f2
prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents:
42886
diff
changeset

820 
(if needs_fairly_sound then typed_helper_suffix 
42881
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

821 
else untyped_helper_suffix), 
dbdfe2d5b6ab
automatically use "metisFT" when typed helpers are necessary
blanchet
parents:
42879
diff
changeset

822 
General), 
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

823 
let val t = th > prop_of in 
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

824 
t > ((case general_type_arg_policy type_sys of 
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

825 
Mangled_Type_Args _ => true 
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

826 
 _ => false) andalso 
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

827 
not (null (Term.hidden_polymorphism 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

828 
? (case types 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

829 
[T] => specialize_type thy (invert_const unmangled_s, 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

830 
 _ => I) 
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

831 
end) 
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

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

833 
map_filter (make_fact ctxt format type_sys false eq_as_iff false) 
42893
fd4babefe3f2
prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents:
42886
diff
changeset

834 
val fairly_sound = is_type_sys_fairly_sound type_sys 
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

835 
in 
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

836 
metis_helpers 
42894
ce269ee43800
further improvements to "poly_{preds,tags}_{bang,query}"  better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents:
42893
diff
changeset

837 
> maps (fn (metis_s, (needs_fairly_sound, ths)) => 
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

838 
if metis_s <> unmangled_s orelse 
42894
ce269ee43800
further improvements to "poly_{preds,tags}_{bang,query}"  better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents:
42893
diff
changeset

839 
(needs_fairly_sound andalso not fairly_sound) then 
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

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

841 
else 
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

842 
ths ~~ (1 upto length ths) 
42893
fd4babefe3f2
prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents:
42886
diff
changeset

843 
> map (dub_and_inst mangled_s needs_fairly_sound) 
fd4babefe3f2
prevent unsound combinator proofs in partially typed polymorphic type systems
blanchet
parents:
42886
diff
changeset

844 
> make_facts (not needs_fairly_sound)) 
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

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

846 
 NONE => [] 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

847 
fun helper_facts_for_sym_table ctxt format type_sys sym_tab = 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

848 
Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

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

850 

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

851 
fun translate_atp_fact ctxt format type_sys keep_trivial = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

852 
`(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of) 
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

853 

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

854 
fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

855 
rich_facts = 
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

856 
let 
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

857 
val thy = Proof_Context.theory_of ctxt 
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

858 
val fact_ts = map (prop_of o snd o snd) rich_facts 
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

859 
val (facts, fact_names) = 
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

860 
rich_facts 
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

861 
> map_filter (fn (NONE, _) => NONE 
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

862 
 (SOME fact, (name, _)) => SOME (fact, name)) 
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

863 
> ListPair.unzip 
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

864 
(* Remove existing facts from the conjecture, as this can dramatically 
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

865 
boost an ATP's performance (for some reason). *) 
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

866 
val hyp_ts = hyp_ts > filter_out (member (op aconv) fact_ts) 
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

867 
val goal_t = Logic.list_implies (hyp_ts, concl_t) 
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

868 
val all_ts = goal_t :: fact_ts 
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

869 
val subs = tfree_classes_of_terms all_ts 
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

870 
val supers = tvar_classes_of_terms all_ts 
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

871 
val tycons = type_consts_of_terms thy all_ts 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

872 
val conjs = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

873 
hyp_ts @ [concl_t] > make_conjecture ctxt format prem_kind type_sys 
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

874 
val (supers', arity_clauses) = 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42586
diff
changeset

875 
if level_of_type_sys type_sys = No_Types then ([], []) 
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

876 
else make_arity_clauses thy tycons supers 
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

877 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 
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

878 
in 
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

879 
(fact_names > map single, (conjs, facts, class_rel_clauses, arity_clauses)) 
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

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

881 

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

882 
fun fo_literal_from_type_literal (TyLitVar (class, name)) = 
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

883 
(true, ATerm (class, [ATerm (name, [])])) 
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

884 
 fo_literal_from_type_literal (TyLitFree (class, name)) = 
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

885 
(true, ATerm (class, [ATerm (name, [])])) 
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

886 

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

887 
fun formula_from_fo_literal (pos, t) = AAtom t > not pos ? mk_anot 
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

888 

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

889 
fun type_pred_combterm ctxt nonmono_Ts type_sys T tm = 
42966
4e2d6c1e5392
more work on parsing LEOII proofs without lambdas
blanchet
parents:
42963
diff
changeset

890 
CombApp (CombConst (`make_fixed_const type_pred_name, T > @{typ bool}, [T]) 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

891 
> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys, 
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

892 
tm) 
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

893 

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

894 
fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum 
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

895 
 var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

896 
accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) 
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

897 
fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false 
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

898 
 is_var_nonmonotonic_in_formula pos phi _ name = 
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

899 
formula_fold pos (var_occurs_positively_naked_in_term name) phi false 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

900 

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

901 
fun mk_const_aterm x T_args args = 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

902 
ATerm (x, map (fo_term_from_typ false) T_args @ args) 
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

903 

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

904 
fun tag_with_type ctxt format nonmono_Ts type_sys T tm = 
42829
1558741f8a72
started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents:
42828
diff
changeset

905 
CombConst (`make_fixed_const type_tag_name, T > T, [T]) 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

906 
> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

907 
> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level 
42829
1558741f8a72
started implementing "shallow" type systems, based on ideas by Claessen et al.
blanchet
parents:
42828
diff
changeset

908 
> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])) 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

909 
and term_from_combterm ctxt format nonmono_Ts type_sys = 
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

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

911 
fun aux site u = 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

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

913 
val (head, args) = strip_combterm_comb u 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

914 
val (x as (s, _), T_args) = 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

915 
case head of 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

916 
CombConst (name, _, T_args) => (name, T_args) 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

917 
 CombVar (name, _) => (name, []) 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

918 
 CombApp _ => raise Fail "impossible \"CombApp\"" 
43000
bd424c3dde46
cleaner handling of equality and proxies (esp. for THF)
blanchet
parents:
42998
diff
changeset

919 
val arg_site = if site = Top_Level andalso is_tptp_equal s then Eq_Arg 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

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

921 
val t = mk_const_aterm x T_args (map (aux arg_site) args) 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

922 
val T = combtyp_of u 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

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

924 
t > (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

925 
tag_with_type ctxt format nonmono_Ts type_sys T 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

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

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

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

929 
in aux end 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

930 
and formula_from_combformula ctxt format nonmono_Ts type_sys 
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

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

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

933 
val higher_order = is_setting_higher_order format type_sys 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

934 
val do_term = term_from_combterm ctxt format nonmono_Ts type_sys Top_Level 
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

935 
val do_bound_type = 
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

936 
case type_sys of 
42722  937 
Simple_Types level => 
42994
fe291ab75eb5
towards supporting nonsimplytyped encodings for TFF and THF (for orthogonality and experiments)
blanchet
parents:
42966
diff
changeset

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

939 
#> mangled_type higher_order false 0 #> SOME 
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

940 
 _ => K NONE 
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

941 
fun do_out_of_bound_type pos phi universal (name, T) = 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

942 
if should_predicate_on_type ctxt nonmono_Ts type_sys 
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

943 
(fn () => should_predicate_on_var pos phi universal name) T then 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

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

945 
> type_pred_combterm ctxt nonmono_Ts type_sys T 
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

946 
> do_term > AAtom > SOME 
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

947 
else 
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

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

949 
fun do_formula pos (AQuant (q, xs, phi)) = 
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

950 
let 
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

951 
val phi = phi > do_formula pos 
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

952 
val universal = Option.map (q = AExists ? not) pos 
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

953 
in 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

954 
AQuant (q, xs > map (apsnd (fn NONE => NONE 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

955 
 SOME T => do_bound_type T)), 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

956 
(if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

957 
(map_filter 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

958 
(fn (_, NONE) => NONE 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

959 
 (s, SOME T) => 
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

960 
do_out_of_bound_type pos phi universal (s, T)) 
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

961 
xs) 
42834
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

962 
phi) 
40f7691d0539
implemented thin versions of "preds" type systems + fixed various issues with type args
blanchet
parents:
42832
diff
changeset

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

964 
 do_formula pos (AConn conn) = aconn_map pos do_formula conn 
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

965 
 do_formula _ (AAtom tm) = AAtom (do_term tm) 
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

966 
in do_formula o SOME end 
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

967 

42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

968 
fun bound_atomic_types format type_sys Ts = 
42727
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

969 
mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal) 
42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

970 
(atp_type_literals_for_types format type_sys Axiom Ts)) 
42727
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

971 

42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

972 
fun formula_for_fact ctxt format nonmono_Ts type_sys 
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

973 
({combformula, atomic_types, ...} : translated_formula) = 
42727
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

974 
combformula 
f365f5138771
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
blanchet
parents:
42726
diff
changeset

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

976 
> formula_from_combformula ctxt format nonmono_Ts type_sys 
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

977 
is_var_nonmonotonic_in_formula true 
42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

978 
> bound_atomic_types format type_sys atomic_types 
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

979 
> close_formula_universally 
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

980 

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

981 
(* Each fact is given a unique fact number to avoid name clashes (e.g., because 
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

982 
of monomorphization). The TPTP explicitly forbids name clashes, and some of 
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

983 
the remote provers might care. *) 
42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

984 
fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys 
42640
879d2d6b05ce
generate tags for simps, intros, and elims in TPTP poblems on demand
blanchet
parents:
42613
diff
changeset

985 
(j, formula as {name, locality, kind, ...}) = 
42680  986 
Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then "" 
987 
else string_of_int j ^ "_") ^ 

42647
59142dbfa3ba
no need to generate fact numbers for polymorphic type systems  this confuses the TPTP exporter
blanchet
parents:
42646
diff
changeset

988 
ascii_of name, 
42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

989 
kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE, 
42879  990 
case locality of 
991 
Intro => intro_info 

992 
 Elim => elim_info 

993 
 Simp => simp_info 

994 
 _ => NONE) 

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

995 

42939  996 
fun formula_line_for_class_rel_clause 
997 
(ClassRelClause {name, subclass, superclass, ...}) = 

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

998 
let val ty_arg = ATerm (`I "T", []) in 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

999 
Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, 
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

1000 
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), 
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

1001 
AAtom (ATerm (superclass, [ty_arg]))]) 
42879  1002 
> close_formula_universally, intro_info, NONE) 
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

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

1004 

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

1005 
fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = 
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

1006 
(true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) 
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

1007 
 fo_literal_from_arity_literal (TVarLit (c, sort)) = 
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

1008 
(false, ATerm (c, [ATerm (sort, [])])) 
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

1009 

42939  1010 
fun formula_line_for_arity_clause 
1011 
(ArityClause {name, prem_lits, concl_lits, ...}) = 

42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

1012 
Formula (arity_clause_prefix ^ ascii_of name, Axiom, 
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

1013 
mk_ahorn (map (formula_from_fo_literal o apfst not 
42895  1014 
o fo_literal_from_arity_literal) prem_lits) 
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

1015 
(formula_from_fo_literal 
42895  1016 
(fo_literal_from_arity_literal concl_lits)) 
42879  1017 
> close_formula_universally, intro_info, NONE) 
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

1018 

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

1019 
fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys 
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

1020 
({name, kind, combformula, ...} : translated_formula) = 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

1021 
Formula (conjecture_prefix ^ name, kind, 
42962
3b50fdeb6cfc
started adding support for THF output (but no lambdas)
blanchet
parents:
42956
diff
changeset

1022 
formula_from_combformula ctxt format nonmono_Ts type_sys 
42939  1023 
is_var_nonmonotonic_in_formula false 
1024 
(close_combformula_universally combformula) 

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

1025 
> close_formula_universally, NONE, NONE) 
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

1026 

42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

1027 
fun free_type_literals format type_sys 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

1028 
({atomic_types, ...} : translated_formula) = 
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

1029 
atomic_types > atp_type_literals_for_types format type_sys Conjecture 
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

1030 
> map fo_literal_from_type_literal 
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

1031 

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

1032 
fun formula_line_for_free_type j lit = 
42577
78414ec6fa4e
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents:
42576
diff
changeset

1033 
Formula (tfree_prefix ^ string_of_int j, Hypothesis, 
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

1034 
formula_from_fo_literal lit, NONE, NONE) 
42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

1035 
fun formula_lines_for_free_types format type_sys facts = 
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

1036 
let 
42956
9aeb0f6ad971
filter Waldmeister facts better  and don't encode type classes as predicates, since it doesn't like conditional equations
blanchet
parents:
42951
diff
changeset

1037 
val litss = map (free_type_literals format type_sys) facts 
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

1038 
val lits = fold (union (op =)) litss [] 
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

1039 
in map2 formula_line_for_free_type (0 upto length lits  1) lits end 
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 

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

1041 
(** Symbol declarations **) 
42544
75cb06eee990
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
blanchet
parents:
42543
diff
changeset

1042 

42574  1043 
fun should_declare_sym type_sys pred_sym s = 
42998
1c80902d0456
fully support all type system encodings in typed formats (TFF, THF)
blanchet
parents:
42994
diff
changeset

1044 
is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso 
42894
ce269ee43800
further improvements to "poly_{preds,tags}_{bang,query}"  better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents:
42893
diff
changeset

1045 
(case type_sys of 
ce269ee43800
further improvements to "poly_{preds,tags}_{bang,query}"  better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents:
42893
diff
changeset

1046 
Simple_Types _ => true 
ce269ee43800
further improvements to "poly_{preds,tags}_{bang,query}"  better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents:
42893
diff
changeset

1047 
 Tags (_, _, Light) => true 
ce269ee43800
further improvements to "poly_{preds,tags}_{bang,query}"  better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents:
42893
diff
changeset

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

1049 

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

1050 
fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) = 
42574  1051 
let 
42698
ffd1ae4ff5c6
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
blanchet
parents:
42697
diff
changeset

1052 
fun add_combterm in_conj tm = 
42574  1053 
let val (head, args) = strip_combterm_comb tm in 
1054 
(case head of< 